Merge pull request #584 from AssetOverflow/feat/comprehension-propositional

feat(comprehend): propositional-logic comprehension (4th domain, flagship oracle)

evals/capability_index/adapters.py

@@ -63,8 +63,15 @@ def comprehension_total_ordering_result() -> DomainResult:
     return DomainResult("comprehension_total_ordering", c, w, r)
 
 
+def comprehension_propositional_result() -> DomainResult:
+    from evals.comprehension.propositional_runner import run
+
+    c, w, r = _counts(run())
+    return DomainResult("comprehension_propositional", c, w, r)
+
+
 #: The reasoning domains currently composed into the index (self-loading lanes).
-#: The three ``comprehension_*`` lanes score the GENERAL comprehension reader
+#: The four ``comprehension_*`` lanes score the GENERAL comprehension reader
 #: (prose -> MeaningGraph -> projection -> independent oracle), so the index now
 #: measures comprehension breadth, not just structured-input reasoning.
 ADAPTERS = (
@@ -74,6 +81,7 @@ ADAPTERS = (
     comprehension_set_membership_result,
     comprehension_syllogism_result,
     comprehension_total_ordering_result,
+    comprehension_propositional_result,
 )
 
 

evals/capability_index/baseline.json

@@ -1,14 +1,22 @@
 {
-  "capability_score": 0.917231,
-  "coverage_geomean": 0.917231,
-  "coverage_micro": 0.993481,
+  "capability_score": 0.928622,
+  "coverage_geomean": 0.928622,
+  "coverage_micro": 0.993582,
   "accuracy_micro": 1.0,
-  "breadth": 6,
+  "breadth": 7,
   "min_domain_coverage": 0.833333,
   "wrong_total": 0,
   "assert_mode_valid": true,
-  "deterministic_digest": "13d7db6c4fc8caed703164cd16c196ecb426a31fb5bcb9658fe630be760179ab",
+  "deterministic_digest": "51df7bba62a035c73bdaf289ea20cded05b66b2f7ca5fd8bbcb04f127d60cadf",
   "domains": [
+    {
+      "domain": "comprehension_propositional",
+      "correct": 12,
+      "wrong": 0,
+      "refused": 0,
+      "coverage": 1.0,
+      "accuracy": 1.0
+    },
     {
       "domain": "comprehension_set_membership",
       "correct": 8,

evals/comprehension/propositional_runner.py

@@ -0,0 +1,71 @@
+"""Score the general comprehension reader on the propositional_logic gold lane.
+
+prose -> comprehend() -> to_deductive_logic() -> independent ROBDD oracle -> verdict
+vs gold. A refusal (unreadable prose, unprojectable, or an oracle "refused" because
+the projected formula could not be evaluated) is NOT a wrong; only a committed
+verdict that disagrees with gold is wrong (must stay 0).
+"""
+
+from __future__ import annotations
+
+import json
+import sys
+from typing import Any
+
+from evals.deductive_logic.oracle import REFUSED, oracle_entailment
+from evals.propositional_logic.runner import _load_cases
+from generate.meaning_graph.projectors import to_deductive_logic
+from generate.meaning_graph.reader import Refusal, comprehend
+
+
+def run() -> dict[str, Any]:
+    cases = _load_cases()
+    correct = wrong = refused = 0
+    wrongs: list[dict[str, Any]] = []
+
+    for case in cases:
+        comp = comprehend(case["text"])
+        if isinstance(comp, Refusal):
+            refused += 1
+            continue
+        projected = to_deductive_logic(comp)
+        if projected is None:
+            refused += 1
+            continue
+        premises, query = projected
+        got = oracle_entailment(premises, query)
+        if got == REFUSED:
+            # the projected formula could not be evaluated -> decline, not a wrong
+            refused += 1
+            continue
+        if got == case.get("gold"):
+            correct += 1
+        else:
+            wrong += 1
+            wrongs.append(
+                {"id": case.get("id"), "got": got, "gold": case.get("gold"), "text": case["text"]}
+            )
+
+    return {
+        "domain": "comprehension_propositional",
+        "total": len(cases),
+        "correct": correct,
+        "wrong": wrong,
+        "refused": refused,
+        "wrongs": wrongs,
+        "counts": {"correct": correct, "wrong": wrong, "refused": refused},
+    }
+
+
+def main() -> int:
+    report = run()
+    print(json.dumps({k: v for k, v in report.items() if k != "wrongs"}, indent=2, sort_keys=True))
+    if report["wrong"]:
+        print("WRONG > 0 — comprehension produced a wrong committed answer:", file=sys.stderr)
+        print(json.dumps(report["wrongs"], indent=2), file=sys.stderr)
+        return 1
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

evals/propositional_logic/runner.py

@@ -0,0 +1,59 @@
+"""Gold-only runner for the staged propositional-logic lane.
+
+The independent arbiter is ``evals.deductive_logic.oracle.oracle_entailment`` (the
+ROBDD-matched brute-force entailment checker). This runner verifies the committed
+gold is exactly that oracle's verdict on each case's ``premises``/``query`` formula
+strings — so the gold cannot drift from the independent oracle.
+"""
+
+from __future__ import annotations
+
+import json
+import sys
+from pathlib import Path
+from typing import Any
+
+from evals.deductive_logic.oracle import oracle_entailment
+
+_CASES = Path(__file__).resolve().parent / "v1" / "cases.jsonl"
+
+
+def _load_cases(path: Path = _CASES) -> list[dict[str, Any]]:
+    return [
+        json.loads(line)
+        for line in path.read_text(encoding="utf-8").splitlines()
+        if line.strip()
+    ]
+
+
+def run(path: Path = _CASES) -> dict[str, Any]:
+    cases = _load_cases(path)
+    failures: list[str] = []
+    for case in cases:
+        got = oracle_entailment(tuple(case["premises"]), case["query"])
+        if got != case.get("gold"):
+            failures.append(f"{case['id']}: oracle={got!r} != gold={case.get('gold')!r}")
+
+    correct = len(cases) - len(failures)
+    return {
+        "domain": "propositional_logic",
+        "total": len(cases),
+        "correct": correct,
+        "wrong": 0,
+        "refused": 0,
+        "gold_integrity_failures": failures,
+        "counts": {"correct": correct, "wrong": 0, "refused": 0},
+    }
+
+
+def main() -> int:
+    report = run()
+    print(json.dumps(report, indent=2, sort_keys=True))
+    if report["gold_integrity_failures"]:
+        print("GOLD INTEGRITY FAILURE", file=sys.stderr)
+        return 1
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

evals/propositional_logic/v1/cases.jsonl

@@ -0,0 +1,12 @@
+{"id":"pl-v1-0001","seed":20260605,"text":"If p then q. p. Therefore q.","premises":["p implies q","p"],"query":"q","gold":"entailed","class":"modus_ponens"}
+{"id":"pl-v1-0002","seed":20260605,"text":"If p then q. Not q. Therefore not p.","premises":["p implies q","not q"],"query":"not p","gold":"entailed","class":"modus_tollens"}
+{"id":"pl-v1-0003","seed":20260605,"text":"If p then q. If q then r. Therefore if p then r.","premises":["p implies q","q implies r"],"query":"p implies r","gold":"entailed","class":"hypothetical_syllogism"}
+{"id":"pl-v1-0004","seed":20260605,"text":"p or q. Not p. Therefore q.","premises":["p or q","not p"],"query":"q","gold":"entailed","class":"disjunctive_syllogism"}
+{"id":"pl-v1-0005","seed":20260605,"text":"p or q. Not q. Therefore p.","premises":["p or q","not q"],"query":"p","gold":"entailed","class":"disjunctive_syllogism"}
+{"id":"pl-v1-0006","seed":20260605,"text":"If p then q. q. Therefore p.","premises":["p implies q","q"],"query":"p","gold":"unknown","class":"affirming_consequent_invalid"}
+{"id":"pl-v1-0007","seed":20260605,"text":"If p then q. Not p. Therefore not q.","premises":["p implies q","not p"],"query":"not q","gold":"unknown","class":"denying_antecedent_invalid"}
+{"id":"pl-v1-0008","seed":20260605,"text":"If p then q. If q then r. p. Therefore r.","premises":["p implies q","q implies r","p"],"query":"r","gold":"entailed","class":"chained_modus_ponens"}
+{"id":"pl-v1-0009","seed":20260605,"text":"If rain then wet. rain. Therefore wet.","premises":["rain implies wet","rain"],"query":"wet","gold":"entailed","class":"modus_ponens_words"}
+{"id":"pl-v1-0010","seed":20260605,"text":"If fire then smoke. Not smoke. Therefore not fire.","premises":["fire implies smoke","not smoke"],"query":"not fire","gold":"entailed","class":"modus_tollens_words"}
+{"id":"pl-v1-0011","seed":20260605,"text":"p or q. p. Therefore not q.","premises":["p or q","p"],"query":"not q","gold":"unknown","class":"inclusive_or_invalid"}
+{"id":"pl-v1-0012","seed":20260605,"text":"sun or moon. Not sun. Therefore moon.","premises":["sun or moon","not sun"],"query":"moon","gold":"entailed","class":"disjunctive_syllogism_words"}

generate/meaning_graph/projectors.py

@@ -132,3 +132,46 @@ def to_total_ordering(comp: Comprehension) -> tuple[dict[str, Any], dict[str, An
     else:
         query = {"kind": "compare", "left": q.arguments[0], "right": q.arguments[1]}
     return structure, query
+
+
+#: Propositional predicates serialized into formula strings for the ROBDD oracle.
+_PROP_PREDICATES = frozenset({"implies", "or", "asserted"})
+
+
+def _formula(predicate: str, args: tuple[str, ...], negated: bool) -> str | None:
+    """Serialize a propositional relation/query into a deductive_logic formula
+    string (keyword operators the oracle tokenizer accepts)."""
+    if predicate == "asserted":
+        return f"not {args[0]}" if negated else args[0]
+    if predicate == "implies":
+        return f"{args[0]} implies {args[1]}"
+    if predicate == "or":
+        return f"{args[0]} or {args[1]}"
+    return None
+
+
+def to_deductive_logic(comp: Comprehension) -> tuple[tuple[str, ...], str] | None:
+    """Project into ``(premises, query)`` formula strings for
+    ``evals.deductive_logic.oracle.oracle_entailment``.
+
+    Returns ``None`` (treated as a refusal) unless the comprehension is purely
+    propositional with >=1 premise and exactly one propositional query — so a
+    categorical/ordering comprehension never leaks into the entailment oracle.
+    """
+    graph = comp.meaning_graph
+    premises: list[str] = []
+    for r in graph.relations:
+        if r.predicate not in _PROP_PREDICATES:
+            return None  # a non-propositional relation -> not this domain
+        formula = _formula(r.predicate, r.arguments, r.negated)
+        if formula is None:
+            return None
+        premises.append(formula)
+
+    prop_queries = [q for q in comp.queries if q.predicate in _PROP_PREDICATES]
+    if not premises or len(comp.queries) != 1 or len(prop_queries) != 1:
+        return None
+    query = _formula(prop_queries[0].predicate, prop_queries[0].arguments, prop_queries[0].negated)
+    if query is None:
+        return None
+    return tuple(premises), query

generate/meaning_graph/reader.py

@@ -303,6 +303,30 @@ def _parse_sort(toks: list[str], detail: str) -> str | None:
     raise _Reject("ambiguous_sort_order", detail)
 
 
+def _parse_propositional(toks: list[str], detail: str) -> tuple[str, tuple[str, ...], bool] | None:
+    """A propositional clause -> (predicate, atom_ids, negated); None if not it.
+
+    Grammar (atoms are single tokens or reserved-free multi-word NPs):
+      ``if <P> then <Q>``  -> ("implies", (P, Q), False)
+      ``not <P>``          -> ("asserted", (P,), True)
+      ``<P> or <Q>``       -> ("or", (P, Q), False)
+      ``<P>`` (one token)  -> ("asserted", (P,), False)
+    Anything else is None (let other templates / refusal handle it)."""
+    if not toks:
+        return None
+    if toks[0] == "if" and "then" in toks:
+        then_idx = toks.index("then")
+        return "implies", (_chunk(toks[1:then_idx], detail), _chunk(toks[then_idx + 1:], detail)), False
+    if toks[0] == "not":
+        return "asserted", (_chunk(toks[1:], detail),), True
+    if "or" in toks:
+        i = toks.index("or")
+        return "or", (_chunk(toks[:i], detail), _chunk(toks[i + 1:], detail)), False
+    if len(toks) == 1:  # bare atomic assertion (single token only — keep the floor)
+        return "asserted", (_chunk(toks, detail),), False
+    return None
+
+
 def comprehend(text: str, source_id: str = "input") -> Comprehension | Refusal:
     """Comprehend *text* into a MeaningGraph + queries, or a typed Refusal."""
     if not text or not text.strip():
@@ -314,7 +338,7 @@ def comprehend(text: str, source_id: str = "input") -> Comprehension | Refusal:
 
     role_kind: dict[str, str] = {}
     span_for: dict[str, MeaningSpan] = {}
-    relations: list[tuple[str, tuple[str, ...], MeaningSpan]] = []
+    relations: list[tuple[str, tuple[str, ...], MeaningSpan, bool]] = []
     queries: list[Query] = []
 
     def claim(entity_id: str, kind: str, span: MeaningSpan) -> None:
@@ -343,7 +367,7 @@ def comprehend(text: str, source_id: str = "input") -> Comprehension | Refusal:
         graph = MeaningGraph(
             entities=entities,
             relations=tuple(
-                Relation(pred, args, sp) for pred, args, sp in relations
+                Relation(pred, args, sp, negated) for pred, args, sp, negated in relations
             ),
         )
     except MeaningGraphError as exc:  # defensive — construction invariants
@@ -357,7 +381,7 @@ def _read_clause(
     question: bool,
     span: MeaningSpan,
     claim,
-    relations: list[tuple[str, tuple[str, ...], MeaningSpan]],
+    relations: list[tuple[str, tuple[str, ...], MeaningSpan, bool]],
     queries: list[Query],
 ) -> None:
     """Match one clause against the templates; mutate accumulators or REFUSE."""
@@ -382,16 +406,24 @@ def _read_clause(
         queries.append(Query("sort", (order,), span))
         return
 
-    # --- syllogism conclusion: "therefore <categorical>" ------------------- #
+    # --- conclusion: "therefore <categorical | propositional>" ------------- #
     if toks[0] == "therefore":
-        parsed = _parse_categorical(toks[1:], clause)
-        if parsed is None:
-            raise _Reject("unreadable_conclusion", clause)
-        predicate, sub, sup = parsed
-        claim(sub, "class", span)
-        claim(sup, "class", span)
-        queries.append(Query(predicate, (sub, sup), span))
-        return
+        rest = toks[1:]
+        categorical = _parse_categorical(rest, clause)
+        if categorical is not None:
+            predicate, sub, sup = categorical
+            claim(sub, "class", span)
+            claim(sup, "class", span)
+            queries.append(Query(predicate, (sub, sup), span))
+            return
+        propositional = _parse_propositional(rest, clause)
+        if propositional is not None:
+            predicate, atoms, negated = propositional
+            for atom in atoms:
+                claim(atom, "proposition", span)
+            queries.append(Query(predicate, atoms, span, negated))
+            return
+        raise _Reject("unreadable_conclusion", clause)
 
     # --- membership query: "is [the] <X> a|an <Y>?" ------------------------ #
     if question and toks[0] == "is":
@@ -429,7 +461,7 @@ def _read_clause(
         predicate, sub, sup = categorical
         claim(sub, "class", span)
         claim(sup, "class", span)
-        relations.append((predicate, (sub, sup), span))
+        relations.append((predicate, (sub, sup), span, False))
         return
 
     # --- membership fact: "[the] <X> is a|an <Y>" -------------------------- #
@@ -442,7 +474,7 @@ def _read_clause(
             cls = _chunk(after[1:], clause)
             claim(name, "individual", span)
             claim(cls, "class", span)
-            relations.append(("member", (name, cls), span))
+            relations.append(("member", (name, cls), span, False))
             return
 
     # --- ordering fact: "<X> [is] <comp> [than] <Y>" ----------------------- #
@@ -451,7 +483,16 @@ def _read_clause(
         lo, hi = comparative
         claim(lo, "item", span)
         claim(hi, "item", span)
-        relations.append(("less", (lo, hi), span))
+        relations.append(("less", (lo, hi), span, False))
+        return
+
+    # --- propositional fact (fallback): if/then, or, not, bare atom -------- #
+    propositional = _parse_propositional(toks, clause)
+    if propositional is not None:
+        predicate, atoms, negated = propositional
+        for atom in atoms:
+            claim(atom, "proposition", span)
+        relations.append((predicate, atoms, span, negated))
         return
 
     raise _Reject("no_template_match", clause)

tests/test_capability_index.py

@@ -87,7 +87,7 @@ def test_empty_index_is_well_defined() -> None:
 
 
 def test_real_lanes_compose_into_the_index_with_wrong_zero() -> None:
-    # The baseline: three structured-input reasoning lanes PLUS the three
+    # The baseline: three structured-input reasoning lanes PLUS the four
     # comprehension lanes (prose -> MeaningGraph -> projection -> independent
     # oracle) compose into the cross-domain index with zero wrong commits.
     from evals.capability_index.adapters import collect_domain_results
@@ -97,7 +97,7 @@ def test_real_lanes_compose_into_the_index_with_wrong_zero() -> None:
     idx = aggregate(list(collection.results))
     assert idx.wrong_total == 0
     assert idx.assert_mode_valid
-    assert idx.breadth == 6
+    assert idx.breadth == 7
     assert {d.domain for d in idx.domains} == {
         "deductive_logic",
         "dimensional",
@@ -105,6 +105,7 @@ def test_real_lanes_compose_into_the_index_with_wrong_zero() -> None:
         "comprehension_set_membership",
         "comprehension_syllogism",
         "comprehension_total_ordering",
+        "comprehension_propositional",
     }
     assert idx.capability_score > 0.5  # real, non-trivial cross-domain capability
 

tests/test_comprehension_propositional.py

@@ -0,0 +1,32 @@
+"""Phase 2b — end-to-end: the comprehension reader scored on propositional_logic.
+
+prose -> comprehend -> to_deductive_logic -> INDEPENDENT ROBDD oracle -> verdict vs
+gold. The load-bearing invariant: wrong == 0 (the reader refuses rather than emit a
+formula that yields a wrong verdict). This lane reads the classic propositional
+argument forms (modus ponens/tollens, hypothetical & disjunctive syllogism) and the
+classic fallacies (affirming the consequent, denying the antecedent), which the
+oracle correctly marks ``unknown``.
+"""
+
+from __future__ import annotations
+
+from evals.comprehension.propositional_runner import run
+
+
+def test_comprehension_propositional_wrong_is_zero() -> None:
+    report = run()
+    assert report["wrong"] == 0, report["wrongs"]
+
+
+def test_comprehension_propositional_has_real_coverage() -> None:
+    report = run()
+    assert report["correct"] > 0
+    assert report["correct"] + report["refused"] == report["total"]
+
+
+def test_comprehension_propositional_full_coverage() -> None:
+    # Every staged case is read end-to-end with zero wrong commits — atoms are
+    # single tokens / reserved-free multi-word NPs, so chunking is unambiguous.
+    report = run()
+    assert report["refused"] == 0
+    assert report["correct"] == report["total"]

tests/test_comprehension_reader.py

@@ -357,3 +357,62 @@ def test_ambiguous_two_np_subset_query_refuses() -> None:
     comp = comprehend("Are all metal objects soft objects?")
     assert isinstance(comp, Refusal)
     assert comp.reason == "ambiguous_subset_query"
+
+
+# --------------------------------------------------------------------------- #
+# Propositional logic — if/then, not, or, bare atom, therefore (deductive_logic)
+# --------------------------------------------------------------------------- #
+
+
+def _qry(comp: Comprehension) -> tuple:
+    return tuple((q.predicate, q.arguments, q.negated) for q in comp.queries)
+
+
+def test_conditional_is_implies() -> None:
+    comp = comprehend("If p then q.")
+    assert isinstance(comp, Comprehension)
+    assert _rel(comp, "implies") == (("implies", ("p", "q")),)
+    assert _entity_kind(comp, "p") == "proposition"
+
+
+def test_bare_atom_is_asserted() -> None:
+    comp = comprehend("p.")
+    assert isinstance(comp, Comprehension)
+    assert _rel(comp, "asserted") == (("asserted", ("p",)),)
+
+
+def test_not_atom_is_negated_assertion() -> None:
+    comp = comprehend("Not p.")
+    assert isinstance(comp, Comprehension)
+    rel = comp.meaning_graph.relations[0]
+    assert (rel.predicate, rel.arguments, rel.negated) == ("asserted", ("p",), True)
+
+
+def test_disjunction_is_or() -> None:
+    comp = comprehend("p or q.")
+    assert isinstance(comp, Comprehension)
+    assert _rel(comp, "or") == (("or", ("p", "q")),)
+
+
+def test_therefore_atom_is_asserted_query() -> None:
+    comp = comprehend("If p then q. p. Therefore q.")
+    assert isinstance(comp, Comprehension)
+    assert _qry(comp) == (("asserted", ("q",), False),)
+
+
+def test_therefore_not_atom_is_negated_query() -> None:
+    comp = comprehend("If p then q. Not q. Therefore not p.")
+    assert isinstance(comp, Comprehension)
+    assert _qry(comp) == (("asserted", ("p",), True),)
+
+
+def test_therefore_conditional_is_implies_query() -> None:
+    comp = comprehend("If p then q. If q then r. Therefore if p then r.")
+    assert isinstance(comp, Comprehension)
+    assert _qry(comp) == (("implies", ("p", "r"), False),)
+
+
+def test_multiword_proposition_chunks_without_reserved_words() -> None:
+    comp = comprehend("If heavy rain then big flood.")
+    assert isinstance(comp, Comprehension)
+    assert _rel(comp, "implies") == (("implies", ("heavy_rain", "big_flood")),)

tests/test_comprehension_wrong_zero_property.py

@@ -23,6 +23,7 @@ from __future__ import annotations
 
 import random
 
+from evals.deductive_logic.oracle import REFUSED, oracle_entailment
 from evals.set_membership.oracle import OracleError as SetError
 from evals.set_membership.oracle import oracle_answer as set_oracle
 from evals.syllogism.oracle import OracleError as SylError
@@ -30,6 +31,7 @@ from evals.syllogism.oracle import oracle_answer as syl_oracle
 from evals.total_ordering.oracle import OracleError as OrdError
 from evals.total_ordering.oracle import oracle_answer as ord_oracle
 from generate.meaning_graph.projectors import (
+    to_deductive_logic,
     to_set_membership,
     to_syllogism,
     to_total_ordering,
@@ -304,3 +306,67 @@ def test_multiword_total_ordering_is_faithful_or_refuses() -> None:
             committed += 1
             assert got == expected, (prose, got, expected)
     assert committed > 50
+
+
+# --------------------------------------------------------------------------- #
+# Propositional logic — faithful entailment verdict or refuse (ROBDD oracle)
+# --------------------------------------------------------------------------- #
+
+_ATOMS = [f"p{i}" for i in range(5)]
+
+
+def _prop_fact(rng):
+    """Return (prose_clause, formula) for a random propositional premise."""
+    kind = rng.choice(["implies", "or", "atom", "not_atom"])
+    if kind == "implies":
+        a, b = rng.sample(_ATOMS, 2)
+        return f"If {a} then {b}.", f"{a} implies {b}"
+    if kind == "or":
+        a, b = rng.sample(_ATOMS, 2)
+        return f"{a} or {b}.", f"{a} or {b}"
+    if kind == "not_atom":
+        a = rng.choice(_ATOMS)
+        return f"Not {a}.", f"not {a}"
+    a = rng.choice(_ATOMS)
+    return f"{a}.", a
+
+
+def _prop_query(rng):
+    """Return (conclusion_prose, formula) for a random propositional query."""
+    kind = rng.choice(["atom", "not_atom", "implies"])
+    if kind == "implies":
+        a, b = rng.sample(_ATOMS, 2)
+        return f"Therefore if {a} then {b}.", f"{a} implies {b}"
+    if kind == "not_atom":
+        a = rng.choice(_ATOMS)
+        return f"Therefore not {a}.", f"not {a}"
+    a = rng.choice(_ATOMS)
+    return f"Therefore {a}.", a
+
+
+def test_propositional_reader_is_faithful_or_refuses() -> None:
+    rng = random.Random(161803)
+    committed = 0
+    for _ in range(400):
+        n = rng.randint(1, 3)
+        facts = [_prop_fact(rng) for _ in range(n)]
+        concl_prose, query_formula = _prop_query(rng)
+        prose = " ".join(p for p, _ in facts) + " " + concl_prose
+        premises = tuple(f for _, f in facts)
+        expected = oracle_entailment(premises, query_formula)
+
+        comp = comprehend(prose)
+        if isinstance(comp, Refusal):
+            continue
+        projected = to_deductive_logic(comp)
+        if projected is None:
+            continue
+        got = oracle_entailment(*projected)
+        if got == REFUSED:
+            continue  # oracle could not evaluate -> decline, not a wrong
+        committed += 1
+        # When the reader commits it must agree with the oracle's verdict on the
+        # ground-truth formulas (unless the ground truth itself was inconsistent).
+        if expected != REFUSED:
+            assert got == expected, (prose, got, expected, premises, query_formula)
+    assert committed > 50

tests/test_meaning_graph_projectors.py

@@ -8,7 +8,11 @@ silent wrong).
 
 from __future__ import annotations
 
-from generate.meaning_graph.projectors import to_syllogism, to_total_ordering
+from generate.meaning_graph.projectors import (
+    to_deductive_logic,
+    to_syllogism,
+    to_total_ordering,
+)
 from generate.meaning_graph.reader import Comprehension, comprehend
 
 
@@ -108,3 +112,32 @@ def test_one_graph_projects_only_to_its_domain() -> None:
     comp = _comp("All mammals are animals. Therefore all mammals are animals.")
     assert to_syllogism(comp) is not None
     assert to_total_ordering(comp) is None
+    assert to_deductive_logic(comp) is None  # categorical relations -> not propositional
+
+
+# --------------------------------------------------------------------------- #
+# to_deductive_logic
+# --------------------------------------------------------------------------- #
+
+
+def test_to_deductive_logic_serializes_formulas() -> None:
+    comp = _comp("If p then q. p. Therefore q.")
+    projected = to_deductive_logic(comp)
+    assert projected is not None
+    premises, query = projected
+    assert set(premises) == {"p implies q", "p"}
+    assert query == "q"
+
+
+def test_to_deductive_logic_serializes_negation_and_disjunction() -> None:
+    comp = _comp("p or q. Not q. Therefore p.")
+    projected = to_deductive_logic(comp)
+    assert projected is not None
+    premises, query = projected
+    assert set(premises) == {"p or q", "not q"}
+    assert query == "p"
+
+
+def test_to_deductive_logic_none_for_categorical_comprehension() -> None:
+    # No propositional relations / query -> nothing askable of the entailment oracle.
+    assert to_deductive_logic(_comp("All mammals are animals.")) is None