IR Logic Utilities API

Status: Generated from current Python docstrings and type hints.

Small propositional-logic helper layer used as a computation backend while Gaia IR remains the persistent semantic contract.

gaia.engine.ir.logic

Logic backends for compiled Gaia IR.

Provides solver-backed analysis of the IR's logical structure. Backends use external libraries (sympy, future Z3/CVC5) while keeping gaia.engine.ir data classes free of solver dependencies.

Current scope

propositional — sympy-based analysis of claim-level Operator graphs (NEGATION/CONJUNCTION/DISJUNCTION/IMPLICATION/EQUIVALENCE/ CONTRADICTION/COMPLEMENT). Treats Knowledge nodes as atoms; does not look inside Claim.formula metadata. diagnostics — FormulaGraph-level inspection for reviewer-facing local formula issues and conservative cross-claim warnings.

Future (out of scope for this PR; tracked separately): predicate — first-order / SMT backends consuming formula_atom metadata for claim-internal predicate / quantifier / arithmetic analysis. smt — cross-cutting analysis combining Operator graph with claim-internal formula metadata.

See docs/specs/2026-05-16-engine-module-reorg-design.md §5 for the three-scope taxonomy.

DiagnosticCondition

Bases: BaseModel

Machine-readable Boolean event associated with a diagnostic.

FormulaDiagnostic

Bases: BaseModel

One formula-level diagnostic emitted for a compiled graph.

FormulaDiagnosticReport

Bases: BaseModel

Collection of formula diagnostics.

has_fatal property

has_fatal: bool

Return whether any diagnostic should block the local claim.

ConditionProbabilityEstimate

Bases: BaseModel

A method-specific probability for one diagnostic Boolean event.

DiagnosticProbability

Bases: BaseModel

Probability scoring result for a diagnostic condition.

inspect_formula_graphs

inspect_formula_graphs(graph: LocalCanonicalGraph, *, include_pairwise: bool = True) -> FormulaDiagnosticReport

Inspect formula graphs and return reviewer-facing logic diagnostics.

Source code in gaia/engine/ir/logic/diagnostics.py

def inspect_formula_graphs(
    graph: LocalCanonicalGraph,
    *,
    include_pairwise: bool = True,
) -> FormulaDiagnosticReport:
    """Inspect formula graphs and return reviewer-facing logic diagnostics."""
    diagnostics: list[FormulaDiagnostic] = []
    projected: list[_ProjectedFormula] = []

    for formula_graph in graph.formula_graphs:
        diagnostics.extend(_redundant_operand_diagnostics(formula_graph))
        try:
            projection = _project_formula_graph(formula_graph)
        except ValueError as error:
            diagnostics.append(_projection_malformed_diagnostic(formula_graph, error))
            continue
        if projection is None:
            diagnostics.append(_projection_unsupported_diagnostic(formula_graph))
            continue
        local_diagnostics = _claim_local_diagnostics(projection)
        diagnostics.extend(local_diagnostics)
        if _is_pairwise_candidate(local_diagnostics):
            projected.append(projection)

    if include_pairwise:
        diagnostics.extend(_pairwise_diagnostics(projected))

    return FormulaDiagnosticReport(diagnostics=diagnostics)

are_equivalent

are_equivalent(graph: LocalCanonicalGraph, left_knowledge_id: str, right_knowledge_id: str) -> bool

Return whether two Gaia propositions are logically equivalent.

Source code in gaia/engine/ir/logic/propositional.py

def are_equivalent(
    graph: LocalCanonicalGraph,
    left_knowledge_id: str,
    right_knowledge_id: str,
) -> bool:
    """Return whether two Gaia propositions are logically equivalent."""
    left = to_sympy_proposition(graph, left_knowledge_id)
    right = to_sympy_proposition(graph, right_knowledge_id)
    return satisfiable(Xor(left, right)) is False

is_satisfiable

is_satisfiable(graph: LocalCanonicalGraph, knowledge_id: str) -> bool

Return whether a Gaia proposition has at least one satisfying assignment.

Source code in gaia/engine/ir/logic/propositional.py

def is_satisfiable(graph: LocalCanonicalGraph, knowledge_id: str) -> bool:
    """Return whether a Gaia proposition has at least one satisfying assignment."""
    return satisfiable(to_sympy_proposition(graph, knowledge_id)) is not False

simplify_proposition

simplify_proposition(graph: LocalCanonicalGraph, knowledge_id: str, *, force: bool = False) -> Any

Return SymPy's simplified Boolean form for a Gaia proposition.

Source code in gaia/engine/ir/logic/propositional.py

def simplify_proposition(
    graph: LocalCanonicalGraph, knowledge_id: str, *, force: bool = False
) -> Any:
    """Return SymPy's simplified Boolean form for a Gaia proposition."""
    return _sympy_simplify_logic(to_sympy_proposition(graph, knowledge_id), force=force)

to_cnf_proposition

to_cnf_proposition(graph: LocalCanonicalGraph, knowledge_id: str, *, simplify: bool = False, force: bool = False) -> Any

Return a CNF SymPy expression for a Gaia proposition.

Source code in gaia/engine/ir/logic/propositional.py

def to_cnf_proposition(
    graph: LocalCanonicalGraph,
    knowledge_id: str,
    *,
    simplify: bool = False,
    force: bool = False,
) -> Any:
    """Return a CNF SymPy expression for a Gaia proposition."""
    return to_cnf(to_sympy_proposition(graph, knowledge_id), simplify=simplify, force=force)

to_dnf_proposition

to_dnf_proposition(graph: LocalCanonicalGraph, knowledge_id: str, *, simplify: bool = False, force: bool = False) -> Any

Return a DNF SymPy expression for a Gaia proposition.

Source code in gaia/engine/ir/logic/propositional.py

def to_dnf_proposition(
    graph: LocalCanonicalGraph,
    knowledge_id: str,
    *,
    simplify: bool = False,
    force: bool = False,
) -> Any:
    """Return a DNF SymPy expression for a Gaia proposition."""
    return to_dnf(to_sympy_proposition(graph, knowledge_id), simplify=simplify, force=force)

to_nnf_proposition

to_nnf_proposition(graph: LocalCanonicalGraph, knowledge_id: str, *, simplify: bool = True) -> Any

Return a negation-normal-form SymPy expression for a Gaia proposition.

Source code in gaia/engine/ir/logic/propositional.py

def to_nnf_proposition(
    graph: LocalCanonicalGraph, knowledge_id: str, *, simplify: bool = True
) -> Any:
    """Return a negation-normal-form SymPy expression for a Gaia proposition."""
    return to_nnf(to_sympy_proposition(graph, knowledge_id), simplify=simplify)

to_sympy_proposition

to_sympy_proposition(graph: LocalCanonicalGraph, knowledge_id: str) -> Any

Expand a Gaia knowledge id into a SymPy Boolean expression.

Knowledge nodes that are not operator conclusions become atomic symbols. Operator conclusions are recursively expanded through Gaia's deterministic propositional operators. The returned SymPy object is a backend representation only; callers should not persist it in Gaia IR.

Source code in gaia/engine/ir/logic/propositional.py

def to_sympy_proposition(graph: LocalCanonicalGraph, knowledge_id: str) -> Any:
    """Expand a Gaia knowledge id into a SymPy Boolean expression.

    Knowledge nodes that are not operator conclusions become atomic symbols. Operator
    conclusions are recursively expanded through Gaia's deterministic propositional
    operators. The returned SymPy object is a backend representation only; callers
    should not persist it in Gaia IR.
    """
    return _to_sympy(
        graph,
        knowledge_id,
        operators=_operator_by_conclusion(graph),
        known_ids=_knowledge_ids(graph),
        cache={},
        stack=set(),
    )

belief_graph_for_formula_scoring

belief_graph_for_formula_scoring(graph: LocalCanonicalGraph) -> FactorGraph

Lower a reviewer scoring graph without formula-generated logic operators.

Formula diagnostics discover warnings from FormulaGraph structure. When those warnings are probability-scored, the belief graph should represent the current belief state before enforcing the warning itself. Compiler-generated formula operators therefore stay out of the scoring graph.

Source code in gaia/engine/ir/logic/probability.py

def belief_graph_for_formula_scoring(graph: LocalCanonicalGraph) -> FactorGraph:
    """Lower a reviewer scoring graph without formula-generated logic operators.

    Formula diagnostics discover warnings from ``FormulaGraph`` structure. When
    those warnings are probability-scored, the belief graph should represent the
    current belief state before enforcing the warning itself. Compiler-generated
    formula operators therefore stay out of the scoring graph.
    """
    belief_graph = graph.model_copy(
        update={
            "operators": [
                operator
                for operator in graph.operators
                if not (operator.metadata or {}).get("formula_lowering")
            ]
        }
    )
    return lower_local_graph(belief_graph)

event_probability

event_probability(expression: dict[str, Any], joint: JointDistribution) -> float

Sum full-joint probability mass satisfying expression.

The joint table is decoded with Gaia's bit-index convention: joint.variables[bit] has value (assignment_index >> bit) & 1.

Source code in gaia/engine/ir/logic/probability.py

def event_probability(expression: dict[str, Any], joint: JointDistribution) -> float:
    """Sum full-joint probability mass satisfying ``expression``.

    The joint table is decoded with Gaia's bit-index convention:
    ``joint.variables[bit]`` has value ``(assignment_index >> bit) & 1``.
    """
    variable_bits = {variable: bit for bit, variable in enumerate(joint.variables)}
    _validate_expression(expression, set(variable_bits))

    return float(
        fsum(
            mass
            for assignment_index, mass in enumerate(joint.probabilities)
            if _evaluate_expression(expression, variable_bits, assignment_index)
        )
    )

score_condition

score_condition(condition: DiagnosticCondition, joint_results: Sequence[JointDistribution | JointQueryUnavailable], *, diagnostic_code: str | None = None) -> DiagnosticProbability

Score a diagnostic condition against available joint query results.

Source code in gaia/engine/ir/logic/probability.py

def score_condition(
    condition: DiagnosticCondition,
    joint_results: Sequence[JointDistribution | JointQueryUnavailable],
    *,
    diagnostic_code: str | None = None,
) -> DiagnosticProbability:
    """Score a diagnostic condition against available joint query results."""
    estimates: list[ConditionProbabilityEstimate] = []
    unavailable: list[JointQueryUnavailable] = []
    probabilities: list[float] = []
    exact_probabilities: list[float] = []

    for result in joint_results:
        if isinstance(result, JointQueryUnavailable):
            unavailable.append(result)
            continue

        probability = event_probability(condition.expression, result)
        estimate = ConditionProbabilityEstimate(
            variables=result.variables,
            method=result.method,
            probability=probability,
            is_exact=result.is_exact,
            basis=result.basis,
            diagnostics=result.diagnostics,
        )
        estimates.append(estimate)
        probabilities.append(probability)
        if result.is_exact:
            exact_probabilities.append(probability)

    return DiagnosticProbability(
        diagnostic_code=diagnostic_code,
        condition_kind=condition.kind,
        variables=condition.variables,
        event_expression=condition.expression,
        estimates=estimates,
        unavailable=unavailable,
        spread=_spread(probabilities),
        exact_spread=_spread(exact_probabilities),
    )

score_diagnostic_conditions

score_diagnostic_conditions(diagnostics: Sequence[FormulaDiagnostic], graph: FactorGraph, *, methods: Sequence[JointQueryMethod] = ('exact', 'junction_tree', 'trw_bp', 'mean_field')) -> list[DiagnosticProbability]

Score diagnostics that carry machine-readable conditions.

This v1 helper intentionally runs the requested joint providers once per scored diagnostic, so its cost model is O(number_of_scored_diagnostics * inference_cost(methods)). Batch reviewer tools that score many warnings should cache provider state above this API or use a future cached query context.

Source code in gaia/engine/ir/logic/probability.py

def score_diagnostic_conditions(
    diagnostics: Sequence[FormulaDiagnostic],
    graph: FactorGraph,
    *,
    methods: Sequence[JointQueryMethod] = ("exact", "junction_tree", "trw_bp", "mean_field"),
) -> list[DiagnosticProbability]:
    """Score diagnostics that carry machine-readable conditions.

    This v1 helper intentionally runs the requested joint providers once per
    scored diagnostic, so its cost model is
    ``O(number_of_scored_diagnostics * inference_cost(methods))``. Batch
    reviewer tools that score many warnings should cache provider state above
    this API or use a future cached query context.
    """
    scored: list[DiagnosticProbability] = []
    for diagnostic in diagnostics:
        condition = diagnostic.condition
        if condition is None:
            continue
        joint_results = compare_joint_over(graph, condition.variables, methods=methods)
        scored.append(
            score_condition(
                condition,
                joint_results,
                diagnostic_code=diagnostic.code,
            )
        )
    return scored