core-labs/core
core-labs/core
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

feat(adr-0249): P3 structural formula→CNF converter (deduction leg) #68

Merged
core-labs merged 1 commit from feat/adr-0249-p3-cnf-converter into main 2026-07-18 19:47:27 +00:00
Conversation 0 Commits 1 Files changed 2 +375
core-labs commented 2026-07-18 19:43:31 +00:00
Owner
Copy link

Third phase of the reader→Hamiltonian compiler arc. P1 (quantity kernel) and P2 (relation compiler) closed the arithmetic leg; this closes the deduction leg — both readers can now reach the corridor.

What it does

evals/logic_cnf_compiler.py — turns propositional formula strings (as emitted by generate.meaning_graph.to_deductive_logic, or any logic_canonical-parseable syntax) into the corridor's CNF PropositionalProblem + a query Clause, consumable by the ratified propositional_entails. compile_entailment(premises, query) is the entry point; formula_to_clauses / query_to_clause / clauses_to_formula are the pieces.

Structural, not truth-table (spike §4.1)

The survey confirmed there is no to_cnf anywhere in the tree, and that logic_canonical's recursive-descent parser is the one production grammar. So the converter reuses that parser for the AST (never re-implements it), then applies the standard sound rewrite itself: eliminate iff/implies → push negations to literals (NNF) → distribute OR over AND, with constant folding, tautological-clause elimination, and a clause budget. It never enumerates assignments and never decides entailment — that stays the corridor's job.

Soundness is proved, not asserted

For a 14-formula panel, the compiled CNF is rendered back to a formula and checked to have the same ROBDD identity as the source via the ratified canonicalize oracle (canonicalize(formula).canonical_key == canonicalize(clauses_to_formula(cnf)).canonical_key). Iff, De Morgan, nested implications, tautologies (P or not P → true) all preserved.

End-to-end agreement, wrong=0

Compiling premises ⊨ query and running it through propositional_entails matches the ROBDD gold (evaluate_entailment) on consistent premises. One honest subtlety, handled explicitly: on inconsistent premises the ROBDD path returns REFUSED, while the corridor returns entailed=True with satisfiable_premises=False (classical ex-falso). Those are different framings of the same fact, so ex-falso is pinned against the corridor's own contract, not cross-checked against the ROBDD path.

Fail-closed + governance

Typed CnfCompileError on conjunctive/constant queries, formulas reducing to false, and CNF-budget overflow; >5 atoms surfaces the corridor's HamiltonianCompileError(atom_count_out_of_range) — the honest ≤5-atom boundary; out-of-regime (quantifiers/predicates) propagates LogicRegimeError. Off-serving (A-04): imports the serving-side parser for its grammar only, lives in the eval quarantine, import-guard pinned. Lives in evals/ because it bridges the generate-side parser to the corridor types (P1/P2 sat in core/physics/ since they needed neither).

Tests

tests/test_adr_0249_logic_cnf_compiler.py — 32/32 green. Soundness panel (14 formulas), entailment agreement (7 consistent cases), modus ponens, ex-falso disclosure, clause shape + determinism, five refusal classes, serve-wiring guard.

[Verification]: uv run python -m pytest tests/test_adr_0249_logic_cnf_compiler.py -q → 32 passed; uv run core test --suite smoke -q → 176 passed.

Third phase of the reader→Hamiltonian compiler arc. P1 (quantity kernel) and P2 (relation compiler) closed the **arithmetic** leg; this closes the **deduction** leg — both readers can now reach the corridor. ## What it does `evals/logic_cnf_compiler.py` — turns propositional formula strings (as emitted by `generate.meaning_graph.to_deductive_logic`, or any `logic_canonical`-parseable syntax) into the corridor's CNF `PropositionalProblem` + a query `Clause`, consumable by the ratified `propositional_entails`. `compile_entailment(premises, query)` is the entry point; `formula_to_clauses` / `query_to_clause` / `clauses_to_formula` are the pieces. ## Structural, not truth-table (spike §4.1) The survey confirmed there is **no `to_cnf` anywhere in the tree**, and that `logic_canonical`'s recursive-descent parser is the one production grammar. So the converter reuses that parser for the AST (never re-implements it), then applies the standard sound rewrite itself: eliminate `iff`/`implies` → push negations to literals (NNF) → distribute OR over AND, with constant folding, tautological-clause elimination, and a clause budget. It never enumerates assignments and never decides entailment — that stays the corridor's job. ## Soundness is proved, not asserted For a 14-formula panel, the compiled CNF is rendered back to a formula and checked to have the **same ROBDD identity** as the source via the ratified `canonicalize` oracle (`canonicalize(formula).canonical_key == canonicalize(clauses_to_formula(cnf)).canonical_key`). Iff, De Morgan, nested implications, tautologies (`P or not P` → `true`) all preserved. ## End-to-end agreement, wrong=0 Compiling `premises ⊨ query` and running it through `propositional_entails` matches the ROBDD gold (`evaluate_entailment`) on consistent premises. One honest subtlety, handled explicitly: on **inconsistent** premises the ROBDD path returns `REFUSED`, while the corridor returns `entailed=True` with `satisfiable_premises=False` (classical ex-falso). Those are different framings of the same fact, so ex-falso is pinned against the corridor's own contract, not cross-checked against the ROBDD path. ## Fail-closed + governance Typed `CnfCompileError` on conjunctive/constant queries, formulas reducing to `false`, and CNF-budget overflow; `>5` atoms surfaces the corridor's `HamiltonianCompileError(atom_count_out_of_range)` — the honest ≤5-atom boundary; out-of-regime (quantifiers/predicates) propagates `LogicRegimeError`. Off-serving (A-04): imports the serving-side parser for its grammar only, lives in the eval quarantine, import-guard pinned. Lives in `evals/` because it bridges the generate-side parser to the corridor types (P1/P2 sat in `core/physics/` since they needed neither). ## Tests `tests/test_adr_0249_logic_cnf_compiler.py` — **32/32 green.** Soundness panel (14 formulas), entailment agreement (7 consistent cases), modus ponens, ex-falso disclosure, clause shape + determinism, five refusal classes, serve-wiring guard. [Verification]: `uv run python -m pytest tests/test_adr_0249_logic_cnf_compiler.py -q` → 32 passed; `uv run core test --suite smoke -q` → 176 passed.
core-labs added 1 commit 2026-07-18 19:43:34 +00:00 
Closes the deduction leg: propositional formula strings (as emitted by
meaning_graph.to_deductive_logic, or any logic_canonical-parseable syntax) →
corridor CNF PropositionalProblem + query Clause, consumable by
propositional_entails.

Structural, not truth-table (spike §4.1): reuses the production ROBDD parser
(generate.logic_canonical — never re-implemented) for the AST, then the standard
sound rewrite — eliminate iff/implies, NNF, distribute OR over AND — with
constant folding, tautological-clause elimination, and a clause budget. The
converter never enumerates assignments and never decides entailment; that stays
the corridor's job.

Soundness proved against the ROBDD oracle: for a 14-formula panel, the compiled
CNF rendered back to a formula has the same canonicalize() identity as the
source. End-to-end entailment through propositional_entails agrees with the
ROBDD gold (evaluate_entailment) wrong=0 on consistent premises; ex-falso
handled per the corridor's own contract (entailed + satisfiable_premises=False,
where the ROBDD path returns REFUSED for inconsistent premises).

Fail-closed: conjunctive/constant queries, formulas reducing to false, and CNF
budget refuse with typed CnfCompileError; >5 atoms surfaces the corridor's
HamiltonianCompileError(atom_count_out_of_range); out-of-regime propagates
LogicRegimeError. Off-serving (A-04), import-guard pinned.

32/32 pins green.

[Verification]: uv run python -m pytest tests/test_adr_0249_logic_cnf_compiler.py -q
core-labs merged commit 309e0ef6c0 into main 2026-07-18 19:47:27 +00:00
core-labs deleted branch feat/adr-0249-p3-cnf-converter 2026-07-18 19:47:28 +00:00
Sign in to join this conversation.
Reviewers
No reviewers
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: core-labs/core#68
No description provided.
Delete branch "feat/adr-0249-p3-cnf-converter"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?