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

feat(deduction-serve): Band v4-CM — conditional-membership fusion, decided (ADR-0259)

Browse source 
Composes v2-EN's connective grammar (if/then, or, and, either) with
v3-MEM's singular-membership sentence reading over one shared
per-individual atom space, so "If Socrates is a man then Socrates is
mortal. Socrates is a man. Therefore Socrates is mortal." decides — the
exact gap ADR-0258 §6.1 reserved. Genuinely fuses the two mechanisms: a
bare universal's instantiated atom can unify (via the same closed
morphology relation) with a connective leaf's atom, deciding arguments
neither band alone could.

- generate/proof_chain/cond_member.py: new reader. A sentence is checked
  for a connective token BEFORE the universal-lead check (so a stray
  connective can never leak into an opaque name/class run); reuses v3-MEM's
  own _parse_singular/_parse_universal verbatim (already negation-aware,
  so no separate negation layer is needed, unlike v2-EN's opaque minter).
  Four new shape-bands (fused/disjunctive/chain/conditional), each earning
  its own SERVE license.
- chat/deduction_surface.py: new fallback tier tried strictly after v3-MEM
  — pure widening, every previously-served argument stays byte-identical.
- evals/deduction_serve/practice/gold.py: 4 new synthetic template groups
  (20 templates), reusing the v3-MEM case generator; intended formulas
  cross-checked against the independent oracle (INV-25).
- evals/deduction_serve/v2_condmem/: 26 hand-authored real-English cases,
  content-disjoint from the synthetic corpus.
- ds-mem-0024 promoted declined -> unknown (not entailed — the antecedent
  is never asserted in that text; this is the first promotion in the
  corpus that doesn't land on entailed).
- Ledger re-sealed to 17 bands; deduction_serve_v1 lane SHA re-pinned
  (surgical single-line edit, not a blanket --update).

Verification: core test --suite deductive 160 passed (31 new reader
tests); practice arena 17 bands x 720 wrong=0, all SERVE-licensed; lane
splits v1 28/28, v2_en 26/26, v2_member 26/26, v2_condmem 26/26; smoke 180
passed; warmed_session 10 passed. Flag deduction_serving_enabled stays
default-off.
This commit is contained in:
Shay 2026-07-24 10:14:00 -07:00
parent dd2245a722
commit ab6da7765e
18 changed files with 1460 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
chat/data/deduction_serve_ledger.json
View file

@ -56,6 +56,34 @@
"t2_verified": 0,
"wrong": 0
},
"en_condmem_chain": {
"correct": 720,
"refused": 0,
"t2_agrees_gold": 0,
"t2_verified": 0,
"wrong": 0
},
"en_condmem_conditional": {
"correct": 720,
"refused": 0,
"t2_agrees_gold": 0,
"t2_verified": 0,
"wrong": 0
},
"en_condmem_disjunctive": {
"correct": 720,
"refused": 0,
"t2_agrees_gold": 0,
"t2_verified": 0,
"wrong": 0
},
"en_condmem_fused": {
"correct": 720,
"refused": 0,
"t2_agrees_gold": 0,
"t2_verified": 0,
"wrong": 0
},
"en_disjunctive": {
"correct": 720,
"refused": 0,
@ -92,7 +120,7 @@
"wrong": 0
}
},
"content_sha256": "3fa864444de56e9e316e8509d3b84648215af73e86540b10199d51182cb7d5ca",
"content_sha256": "6285a423957bc9a3a6a562515a338dfd6f36188ac00f45c1a6ea979c4e3cc710",
"note": "Sealed-practice committed ledger for deduction serving (ADR-0256). Engine reads, never writes. Ceilings stay at safe defaults (theta_SERVE=0.99). A band earns SERVE by demonstrated pipeline reliability (reader+projector+engine) at volume >= 657 committed.",
"provenance": "evals.deduction_serve.practice.runner.seal_ledger",
"schema": "deduction_serve_ledger_v1"

31
chat/deduction_surface.py
View file

@ -27,6 +27,13 @@ Bands (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md):
mortal."), read by ``generate.proof_chain.member`` via per-individual
propositional lowering and decided by the same engine. Tried strictly AFTER
v2-EN (which guards these shapes out) — again a pure widening tier.
- Band v4-CM (ADR-0259) — conditional-membership fusion arguments ("If
Socrates is a man then Socrates is mortal. Socrates is a man. Therefore
Socrates is mortal."), composing v2-EN's connective grammar with v3-MEM's
singular-membership sentence reading over one shared per-individual atom
space, read by ``generate.proof_chain.cond_member``. Tried strictly AFTER
v3-MEM (which guards these shapes out via ``mixed_structure_out_of_band``)
— again a pure widening tier.
Fail-closed (INV-34): once ``looks_like_deductive_argument`` fires, every path
below returns a committed, honest surface — reader refusal, out-of-band shape,
@ -44,6 +51,7 @@ from core.reliability_gate import LicenseDecision
from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism
from generate.meaning_graph.reader import Comprehension, comprehend
from generate.proof_chain.categorical import CategoricalError, decide_syllogism
from generate.proof_chain.cond_member import CondMemberArgument, read_cond_member_argument
from generate.proof_chain.english import EnglishArgument, read_english_argument
from generate.proof_chain.entail import evaluate_entailment_with_trace
from generate.proof_chain.member import MemberArgument, read_member_argument
@ -132,6 +140,9 @@ def deduction_grounded_surface(
member = _member_band_surface(text, license_lookup)
if member is not None:
return member
cond_member = _cond_member_band_surface(text, license_lookup)
if cond_member is not None:
return cond_member
return _READER_REFUSAL_SURFACE.format(reason=comp.reason)
# Band v1 — propositional argument.
projected = to_deductive_logic(comp)
@ -160,6 +171,10 @@ def deduction_grounded_surface(
member = _member_band_surface(text, license_lookup)
if member is not None:
return member
# Band v4-CM fallback — the conditional-membership shapes v3-MEM guards out.
cond_member = _cond_member_band_surface(text, license_lookup)
if cond_member is not None:
return cond_member
return _OUT_OF_BAND_SURFACE
@ -189,6 +204,22 @@ def _member_band_surface(text: str, license_lookup: _LicenseLookup) -> str | Non
return _license_gate(surface, arg.band, license_lookup)
def _cond_member_band_surface(text: str, license_lookup: _LicenseLookup) -> str | None:
"""Band v4-CM (ADR-0259): read *text* as a conditional-membership argument
(v2-EN connectives over v3-MEM singular-membership leaves), and decide
with the same verified ROBDD engine; ``None`` when the reader refuses (the
caller keeps its pre-existing honest surface — this band only ever widens
what is decided). Reuses ``render_entailment_member`` unchanged: its
UNKNOWN scoping is exactly as accurate here (every clause is read all the
way to individual+class; connectives add no new hidden structure)."""
arg = read_cond_member_argument(text)
if not isinstance(arg, CondMemberArgument):
return None
trace = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula)
surface = render_entailment_member(trace, arg.premise_texts, arg.query_text)
return _license_gate(surface, arg.band, license_lookup)
def _license_gate(surface: str, band: str, license_lookup: _LicenseLookup) -> str:
"""Serve *surface* authoritatively iff *band* holds a SERVE license; else
serve the same sound answer DISCLOSED (hedged). The one place the earned-

1
core/cli_test.py
View file

@ -179,6 +179,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = {
"tests/test_categorical_decider.py",
"tests/test_english_argument_reader.py",
"tests/test_member_argument_reader.py",
"tests/test_cond_member_argument_reader.py",
"tests/test_deduction_serve_e2e.py",
),
"full": ("tests/",),

163
docs/adr/ADR-0259-conditional-membership-fusion-band.md Normal file
View file

@ -0,0 +1,163 @@
# ADR-0259 — Conditional-membership fusion band (Band v4-CM)
- **Status:** Proposed
- **Date:** 2026-07-23
- **Relates to:** ADR-0258 (Band v3-MEM — this is its scope-out #1), ADR-0257
(Band v2-EN — the connective grammar this band reuses), ADR-0256 (earned
license), ADR-0201 (ROBDD keystone), ADR-0175/0199 (calibrated learning /
arena)
## 1. Context
ADR-0258 §6.1 reserved conditional–membership fusion as a future band:
> "If Socrates is a man then Socrates is mortal. Socrates is a man.
> Therefore Socrates is mortal."
Band v3-MEM refuses this — `mixed_structure_out_of_band` — because its
per-sentence grammar treats a connective token (`if`/`then`/`or`/`and`/
`either`) anywhere in a sentence as announcing structure that band does not
compose. Band v2-EN refuses the same text for the complementary reason:
its opaque-atom minter explicitly rejects `is [a|an]` clauses
(`membership_shape_out_of_band`) rather than flattening membership
structure it cannot read. Each band is individually sound and, by design,
refuses exactly what the other reads — the gap is the composition, not
either reader's engine.
## 2. Decision
Add `generate/proof_chain/cond_member.py` — a third reader, tried strictly
AFTER Bands v1 / v1b / v2-EN / v3-MEM (a fallback tier; every previously
served argument stays byte-identical) — that composes v2-EN's connective
grammar (`if/then`, `or`, `and`, `either` sugar, top-level `and`-splitting)
with v3-MEM's singular membership sentence reading, over the SAME
per-individual atom space:
- **Sentence dispatch** (closed, ordered): a bare top-level `X and Y`
premise (no `if`/`or` anywhere) splits into independent singular
records, exactly as v2-EN does — semantically conjoining, keeping the
connective inventory the shape-bands classify over uncluttered. Any
OTHER sentence containing a connective token is parsed by the ported
junction/conditional grammar below. A universal-lead (`all|every|each|
no`) sentence with NO connective token is a bare universal, read
UNCHANGED by v3-MEM's own `_parse_universal`. Everything else is a bare
singular fact, read UNCHANGED by v3-MEM's own `_parse_singular` (which
already normalizes every negation form this band needs — leading `not`,
the sentential `it is not the case that` prefix, and copular `is not`).
Checking for a connective token BEFORE the universal-lead dispatch (not
after) is load-bearing: it is what stops a connective token from ever
silently leaking into an opaque name/class run.
- **Connective grammar over membership leaves:** `if <A> then <B>` and
`<A> or <B>` / `<A> and <B>` (with `either` as sugar, mixed `and`+`or` at
one level refused as `ambiguous_and_or`, a conditional nested inside
another refused as `nested_conditional` — identical restrictions to
v2-EN, ported verbatim) build a small formula tree (`_Lit` / `_And` /
`_Or` / `_Implies`) whose LEAVES are v3-MEM singular facts, not opaque
atoms. Because `_parse_singular` is negation-aware on its own, this
band's grammar needs no separate negation layer — v2-EN needs one only
because ITS leaf-miller (`_AtomTable.mint`) is negation-blind.
- **A conclusion stays a single singular fact** (optionally negated),
matching v3-MEM's existing discipline exactly: a universal or
connective-shaped conclusion refuses
(`universal_conclusion_out_of_band` / new `compound_conclusion_out_of_band`)
rather than attempting a compound render.
- **One shared per-individual atom space:** every singular fact — whether
a bare sentence, an and-split part, or a leaf nested inside a connective
tree — contributes to the SAME two-pass lowering v3-MEM already performs
(collect named individuals and closed-morphology class-groups first,
THEN mint one opaque atom per attested `(individual, class)` pair, THEN
instantiate every bare universal at every named individual). A bare
universal may now instantiate at an individual named ONLY inside a
connective's leaf, and a connective's leaf atom may now UNIFY with an
atom a bare universal's instantiation also produced — this atom-sharing
across the two mechanisms is the fusion the band is named for, and nothing
about it is a new soundness claim: it is the same per-individual
instantiation ADR-0258 §3 already proved sound, applied to a strictly
larger set of premise formulas.
- **Four new shape-bands**, priority order first-match: `en_condmem_fused`
(a bare universal coexists with a connective sentence — the mechanism
above genuinely fires), `en_condmem_disjunctive` (an `or` appears
anywhere in any connective sentence), `en_condmem_chain` (two or more
connective sentences, no universal, no `or`), `en_condmem_conditional`
(the base case — exactly one `if/then`, no universal, no `or`). A
successfully-decided argument in this band always contains at least one
connective sentence — every other reason v3-MEM would refuse also makes
THIS reader refuse identically (it reuses v3-MEM's own
`_parse_universal`/`_parse_singular`, guards included), so there is no
connective-free case this band could newly decide; no fifth "atomic"
band is needed.
## 3. Why the composition is sound (the load-bearing argument)
1. **Nothing here is a new inference rule.** Every connective (`&`, `|`,
`->`) is standard propositional structure the ROBDD engine already
decides; every leaf is a v3-MEM singular-membership atom, minted and
linked by the IDENTICAL closed morphology relation ADR-0258 §3 already
proved sound and (for this fragment) complete. Composing them is
substitution of one sound reading's atoms into another sound reading's
connective positions — the propositional engine's soundness does not
care which reader supplied which formula string.
2. **Universal instantiation stays sound when the instantiated individual
is named only inside a connective.** ADR-0258 §3's argument — every
first-order model of `∀x(C1(x)→C2(x))` satisfies the instantiation at
every domain element, so at every NAMED individual in particular — does
not depend on WHERE in the argument that individual's name appears. An
individual introduced solely as the subject of an `if`-clause leaf is
still a named individual; instantiating a bare universal at it is still
a sound consequence of the universal, exactly as if it had appeared in
its own bare sentence.
3. **Completeness is preserved for the same closed fragment.** The
fragment is unchanged from ADR-0258 (singular literals + A/E
universals, Boolean reading, no existential import) with one syntactic
widening: singular literals may now be combined by `&`/`|`/`->` before
appearing as a premise or antecedent/consequent. A propositional
countermodel still lifts to a first-order countermodel over exactly
the named individuals, by the identical argument — connectives among
already-Boolean atoms do not change what "every element is a named
individual" needs to guarantee. UNKNOWN therefore still means genuinely
not forced within the disclosed reading, and the surface still scopes
itself exactly as v3-MEM's does (reused verbatim — see §4).
4. **The refusal vocabulary stays a strict superset of v3-MEM's, plus
v2-EN's connective-shape guards.** `nested_conditional` and
`ambiguous_and_or` are v2-EN's own restrictions, ported unchanged
(English `and`/`or` scope genuinely is ambiguous when mixed; a
conditional nested inside another is refused rather than guessed at,
in both bands identically). `compound_conclusion_out_of_band` is new
and narrow: it exists only to keep the conclusion a single renderable
fact, not to hide any inference.
## 4. What the earned licenses certify; rendering
Same posture as ADR-0258 §4: the license certifies reader fidelity, not
engine soundness. `render_entailment_member` (ADR-0258) is reused
UNCHANGED for this band's surface — its UNKNOWN scoping ("reading each
name as one individual and each class word at face value…") is exactly as
accurate here, since every clause in this band's arguments is read all the
way down to individual+class; connectives introduce no additional hidden
structure the surface would need to disclose. No new render function is
added.
## 5. Scope-outs (deliberate)
1. **A universal clause cannot be nested inside a connective** — only a
bare top-level universal sentence instantiates; `if all men are
mortal then …` refuses (typed, via the same connective-shape-first
dispatch that protects bare universals from silent corruption).
Composing a QUANTIFIED antecedent/consequent is a larger, separate
question (it would need bound-variable tracking across clauses, not
just shared individuals) and is left for a future band if a real case
ever needs it.
2. **Existential premises, tense, verb predicates, identity/definite
descriptions** — unchanged scope-outs, inherited from ADR-0258 §6
via the reused `_parse_singular`/`_parse_universal`.
3. **Flag posture unchanged:** rides `deduction_serving_enabled` (default
off); no new flag.
## 6. Verification
- `uv run core test --suite deductive -q` — reader contract, surfaces,
license, all four lane splits, e2e through `ChatRuntime`.
- Practice arena: 17 bands × 720 = 12,240 cases, wrong=0 required for every
band; ledger re-sealed (`chat/data/deduction_serve_ledger.json`).
- Eval lane: v1 28/28, v2_en 26/26, v2_member 26/26, v2_condmem new —
wrong=0; report re-pinned (`scripts/verify_lane_shas.py`).

124
docs/research/conditional-membership-fusion-band-2026-07-23.md Normal file
View file

@ -0,0 +1,124 @@
# Band v4-CM: conditional-membership fusion, decided (ADR-0259)
**Date:** 2026-07-23 · **Arc:** deduction-serve, band 5 of the cascade
**ADR:** ADR-0259 (Proposed) · **Flag:** `deduction_serving_enabled` (default off, unchanged)
## What CORE serves now (flag-on transcripts)
Decided, from the real `core chat` spine, over the user's own sentences —
the exact gap ADR-0258 §6.1 reserved:
> **If Socrates is a man then Socrates is mortal. Socrates is a man.
> Therefore Socrates is mortal.**
> → Given: if socrates is a man then socrates is mortal; socrates is a man.
> Your premises entail: socrates is mortal.
The genuine fusion case — a bare universal's instantiated atom UNIFYING
with a connective leaf's atom, something neither v2-EN nor v3-MEM alone can
decide:
> **All men are mortal. If Socrates is a philosopher then Socrates is a
> man. Socrates is a philosopher. Therefore Socrates is mortal.**
> → …Your premises entail: socrates is mortal.
> **If Socrates is a man then Socrates is mortal. Therefore Socrates is
> mortal.** *(the antecedent is never asserted)*
> → …Reading each name as one individual and each class word at face
> value, your premises don't settle whether socrates is mortal — it holds
> in some cases and fails in others.
That last one is `ds-mem-0024` — the eval-lane case pinned `declined`
purely for want of a reading band, now promoted. It is the **first
promotion in this corpus that does not land on `entailed`**: the band now
reads the text, and the honest answer for THAT specific text is UNKNOWN
(no premise ever asserts the antecedent). Promotion means "now decided
correctly," not "now decided favorably."
## Mechanism (one new module, everything else reused)
`generate/proof_chain/cond_member.py` composes v2-EN's connective grammar
(`if/then`, `or`, `and`, `either`) with v3-MEM's singular-membership
sentence reading, over ONE shared per-individual atom space. Concretely:
a sentence is checked for a connective token BEFORE the universal-lead
check (so a stray connective can never leak into an opaque universal/
singular name run); a bare top-level `and` premise still splits into
independent facts (v2-EN's own discipline); everything else containing
`if`/`then`/`or`/`either` builds a small formula tree (`Lit`/`And`/`Or`/
`Implies`) whose LEAVES are v3-MEM singular facts — parsed by v3-MEM's own
`_parse_singular`, reused verbatim, which is already negation-aware (unlike
v2-EN's opaque-atom minter, so this band needs no separate negation layer).
The SAME two-pass lowering v3-MEM already performs — collect named
individuals and closed-morphology class-groups, THEN mint atoms, THEN
instantiate every bare universal at every named individual — now also
scans leaves nested inside connective trees, which is what lets a
universal instantiate at an individual named only inside an `if`-clause,
and lets a connective leaf's atom unify with one a universal's
instantiation also produced.
**Soundness (ADR-0259 §3):** nothing here is a new inference rule — every
connective is standard propositional structure the ROBDD engine already
decides; every leaf is minted and linked by the IDENTICAL closed
morphology relation ADR-0258 §3 already proved sound and, for this
fragment, complete. Universal instantiation stays sound regardless of
WHERE a named individual's name appears in the argument; composing
connectives over already-Boolean membership atoms does not change what
"every element is a named individual" needs to guarantee for completeness.
UNKNOWN is rendered by `render_entailment_member` UNCHANGED — no new
render function; its scoping is exactly as accurate here.
## Earned, not flagged (ADR-0256 discipline)
- Four new shape-bands — `en_condmem_fused/disjunctive/chain/conditional`
— each earned SERVE at the arena: **17 bands × 720 = 12,240 cases,
wrong=0**, reliability 0.99087 ≥ θ_SERVE=0.99; ledger re-sealed
(`chat/data/deduction_serve_ledger.json`, 17 bands, sha `6285a423…`).
Priority order fused > disjunctive > chain > conditional; a successfully-
decided argument in this band always contains ≥1 connective sentence (any
other refusal reason v3-MEM would hit, this band hits identically, via
the SAME reused guards), so no fifth "atomic" band is needed.
- Arena gold is by-construction and cross-checked against the truth-table
oracle over each template's INTENDED formulas — no reader in the loop
(INV-25). The FUSED templates specifically encode the cross-mechanism
unification (verified by hand-trace against the real reader before
writing gold, then confirmed by the independent oracle).
- New hand-authored real-English lane `evals/deduction_serve/v2_condmem/`
(26 cases, content-disjoint): **26/26**, alongside v1 **28/28**, v2_en
**26/26**, and v2_member **26/26** (wrong=0 everywhere; the promoted
`ds-mem-0024` now scores against its corrected `unknown` gold).
## Verification
- `uv run core test --suite deductive -q`: **160 passed** (31-test reader
contract new: flagship, modus tollens, both disjunctive spellings, the
and-split-is-not-a-connective case, two-hop chains, the fusion mechanism
itself — including a no-leak-across-individuals check — band
classification, the full refusal vocabulary, both honesty caps,
determinism).
- Practice arena: `all_bands_serve_licensed=True wrong_is_zero=True` (17
bands).
- Lane splits: v1 28/28 · v2_en 26/26 · v2_member 26/26 (post-promotion) ·
v2_condmem 26/26.
- Smoke suite: **180 passed**. Warmed-session lane: **10 passed**.
## A wrinkle worth surfacing
`scripts/verify_lane_shas.py --update` was run once to re-pin
`deduction_serve_v1` and, because the flag updates every lane in one pass,
it also silently rewrote `miner_loop_closure`, `curriculum_loop_closure`,
and `demo_composition`'s pins and DROPPED `public_demo`'s pin entirely
(that lane errored — `all_claims_supported=False` — a known flake). Those
three rewrites were reverted; **only** the `deduction_serve_v1` line was
hand-edited to the freshly-computed SHA. The three lanes' drift is
real, pre-existing, and unrelated to this arc (this worktree branched
directly off the just-merged main) — it is reported here, not fixed, since
diagnosing it is outside this band's scope and blind re-pinning is exactly
what the tool's own remediation text warns against.
## Scope-outs (deliberate, ADR-0259 §5)
A universal clause cannot be nested inside a connective (only a bare
top-level universal instantiates) — composing a quantified antecedent/
consequent would need bound-variable tracking across clauses, a larger
question left for a future band if a real case needs it. Existential
premises, tense, verb predicates, identity/definite descriptions remain
out of band, inherited unchanged from ADR-0258.

27
evals/deduction_serve/contract.md
View file

@ -8,8 +8,9 @@ The **production serving decider** — the exact pipeline
`comprehend` (reader) → the band cascade — `to_deductive_logic` (Band v1)
→ `to_syllogism` + the categorical decider (Band v1b, ADR-0256) →
`read_english_argument` (Band v2-EN, ADR-0257) → `read_member_argument`
(Band v3-MEM, ADR-0258) — with `evaluate_entailment_with_trace` (the
ROBDD engine, ADR-0201/ADR-0218) deciding every band.
(Band v3-MEM, ADR-0258) → `read_cond_member_argument` (Band v4-CM,
ADR-0259) — with `evaluate_entailment_with_trace` (the ROBDD engine,
ADR-0201/ADR-0218) deciding every band.
`evals/deduction_serve/runner.py::decide` calls these functions directly
(typed outcome, not rendered prose) — the same production decision the
composer makes, without re-deriving the presentation step
@ -23,6 +24,11 @@ against wording-only changes.
content disjoint from the synthetic practice lexicon.
- `v2_member/` — hand-authored membership/universal arguments (ADR-0258),
incl. real nouns across every number-link row-type.
- `v2_condmem/` — hand-authored conditional-membership arguments
(ADR-0259): v2-EN's connective grammar composed over v3-MEM's singular-
membership sentence reading, incl. genuine universal+connective fusion
cases (a bare universal's instantiated atom unifying with a connective
leaf's atom).
This is **distinct** from two existing lanes that sound similar:
@ -63,7 +69,9 @@ corpus, since every committed case reads as an argument by design).
Boundaries are DISCOVERED as declines, then PROMOTED to decided gold when
a later band earns the shape (the corpus keeps the case, renamed
`…_formerly_out_of_band`):
`…_formerly_out_of_band`). Promotion does not always mean "→ entailed":
the promoted gold is whatever the newly-earned band actually, honestly
decides for that exact text.
- **Nested negation inside `if/then`** — a shared-reader grammar limit
(`not` is reserved inside if/then slots); `ds-v1-0006` declined until
@ -74,10 +82,21 @@ a later band earns the shape (the corpus keeps the case, renamed
Band v1b since ADR-0256.
- **`is a` membership** — `ds-en-0022` declined until Band v3-MEM decided
it (promoted, ADR-0258).
- **A bare conditional over membership clauses** — `ds-mem-0024`
(`"If Socrates is a man then Socrates is mortal. Therefore Socrates is
mortal."`) declined (`mixed_structure_out_of_band`) until Band v4-CM
landed (ADR-0259), which reads it — but the antecedent is never
asserted, so its honest verdict is **UNKNOWN**, not entailed. Promoted
declined → unknown, renamed `conditional_no_anchor_formerly_out_of_band`
— the first promotion in this corpus that does not land on `entailed`,
because the promoted band's own correct answer for THIS text is a
non-commitment, not a new capability to showcase.
- **Still-open declines** (honest, typed): verb-phrase negation
(`ds-en-0023/0024`), ambiguous `and`/`or` scope (`ds-en-0025`), nested
conditionals (`ds-en-0026`), existential quantifiers / bare plurals /
definite descriptions / relative clauses / tense (`ds-mem-0020…0026`).
definite descriptions / relative clauses / tense
(`ds-mem-0020…0023/0025/0026`), a universal clause nested inside a
connective, compound conclusions (`ds-cm-0020…0026`).
## Reproduce

144
evals/deduction_serve/practice/gold.py
View file

@ -33,6 +33,7 @@ from core.learning_arena.protocols import Problem
from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism
from generate.meaning_graph.reader import Comprehension, comprehend
from generate.proof_chain.categorical import CategoricalError, decide_syllogism
from generate.proof_chain.cond_member import CondMemberArgument, read_cond_member_argument
from generate.proof_chain.english import EnglishArgument, read_english_argument
from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
from generate.proof_chain.member import MemberArgument, read_member_argument
@ -45,6 +46,10 @@ from generate.proof_chain.shape import (
EN_ATOMIC,
EN_CONDITIONAL_CHAIN,
EN_CONDITIONAL_SINGLE,
EN_CONDMEM_CHAIN,
EN_CONDMEM_CONDITIONAL,
EN_CONDMEM_DISJUNCTIVE,
EN_CONDMEM_FUSED,
EN_DISJUNCTIVE,
EN_MEMBER_ATOMIC,
EN_MEMBER_CHAIN,
@ -387,12 +392,122 @@ _MEM_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = {
),
}
#: Ledger band order: the five v1 bands, the four v2-EN bands, then the four
#: v3-MEM bands.
# --- Band v4-CM (ADR-0259): conditional-membership synthetic corpus ----------
#
# Reuses the v3-MEM case generator (``_mem_case``) directly — same names/
# classes/states pool, no new lexicon needed. Composes v2-EN's connective
# grammar with v3-MEM's singular-membership sentence reading over the SAME
# per-individual atom space; the FUSED templates specifically exercise a bare
# universal instantiation UNIFYING (via the closed morphology relation) with
# an atom a connective's leaf also produced — the mechanism this band adds.
_CM_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = {
EN_CONDMEM_CONDITIONAL: (
# Modus ponens over membership atoms.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.",
("ca implies cb", "ca"), "cb"),
# Modus tollens.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is not {st}. Therefore {n1} is not a {c1[0]}.",
("ca implies cb", "not cb"), "not ca"),
# Direct contradiction of the consequent.
("refuted",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is not {st}.",
("ca implies cb", "ca"), "not cb"),
# Affirming the consequent — classic non-sequitur.
("unknown",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is {st}. Therefore {n1} is a {c1[0]}.",
("ca implies cb", "cb"), "ca"),
# Denying the antecedent — classic non-sequitur.
("unknown",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is not a {c1[0]}. Therefore {n1} is not {st}.",
("ca implies cb", "not ca"), "not cb"),
# No anchor at all.
("unknown",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. Therefore {n1} is a {c1[0]}.",
("ca implies cb",), "ca"),
),
EN_CONDMEM_DISJUNCTIVE: (
# Disjunctive syllogism over membership atoms.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]} or {n1} is a {c2[0]}. {n1} is not a {c1[0]}. Therefore {n1} is a {c2[0]}.",
("ca or cb", "not ca"), "cb"),
# "either" spelling, other disjunct.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"Either {n1} is a {c1[0]} or {n1} is a {c2[0]}. {n1} is not a {c2[0]}. Therefore {n1} is a {c1[0]}.",
("ca or cb", "not cb"), "ca"),
# Constructive dilemma.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]} or {n1} is a {c2[0]}. Therefore {n1} is {st}.",
("ca implies cc", "cb implies cc", "ca or cb"), "cc"),
# Eliminating one disjunct entails the other's negation is refuted.
("refuted",
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]} or {n1} is a {c2[0]}. {n1} is not a {c1[0]}. Therefore {n1} is not a {c2[0]}.",
("ca or cb", "not ca"), "not cb"),
# A bare disjunction settles neither disjunct.
("unknown",
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]} or {n1} is a {c2[0]}. Therefore {n1} is a {c1[0]}.",
("ca or cb",), "ca"),
),
EN_CONDMEM_CHAIN: (
# Two-hop modus ponens across two connective sentences.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.",
("ca implies cb", "cb implies cc", "ca"), "cc"),
# Two-hop modus tollens.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is not {st}. Therefore {n1} is not a {c1[0]}.",
("ca implies cb", "cb implies cc", "not cc"), "not ca"),
# Two-hop chain onto a MEMBERSHIP conclusion (not a state).
("entailed",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is a {c3[0]}. {n1} is a {c1[0]}. Therefore {n1} is a {c3[0]}.",
("ca implies cb", "cb implies cc", "ca"), "cc"),
# Chain contradiction.
("refuted",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is not {st}.",
("ca implies cb", "cb implies cc", "ca"), "not cc"),
# Chain with no anchor.
("unknown",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is {st}. Therefore {n1} is {st}.",
("ca implies cb", "cb implies cc"), "cc"),
),
EN_CONDMEM_FUSED: (
# The mechanism: a bare universal's instantiated atom UNIFIES (via
# the closed morphology relation) with a connective leaf's atom —
# neither mechanism alone would decide this.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"All {c1[1]} are {c2[1]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.",
("ca implies cb", "cb implies cc", "ca"), "cc"),
# Reversed sentence order — connective first, universal second.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. All {c2[1]} are {c1[1]}. {n1} is a {c2[0]}. Therefore {n1} is {st}.",
("ca implies cb", "cc implies ca", "cc"), "cb"),
# Universal first, singular second, connective third.
("entailed",
lambda n1, n2, c1, c2, c3, st: f"All {c1[1]} are {c2[1]}. {n1} is a {c1[0]}. If {n1} is a {c2[0]} then {n1} is {st}. Therefore {n1} is {st}.",
("ca implies cb", "ca", "cb implies cc"), "cc"),
# Fused chain contradiction.
("refuted",
lambda n1, n2, c1, c2, c3, st: f"All {c1[1]} are {c2[1]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is not {st}.",
("ca implies cb", "cb implies cc", "ca"), "not cc"),
# The universal binds a DIFFERENT individual than the connective and
# query concern — instantiating it for one individual must not leak
# into another's conclusion.
("unknown",
lambda n1, n2, c1, c2, c3, st: f"All {c1[1]} are {st}. If {n2} is a {c2[0]} then {n2} is a {c1[0]}. {n1} is a {c1[0]}. Therefore {n2} is {st}.",
("ca implies cb", "cc implies cd", "ce implies ca", "cc"), "cb"),
),
}
#: Ledger band order: the five v1 bands, the four v2-EN bands, the four
#: v3-MEM bands, then the four v4-CM bands.
_ALL_BANDS: tuple[str, ...] = (
CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC, CATEGORICAL,
EN_CONDITIONAL_SINGLE, EN_CONDITIONAL_CHAIN, EN_DISJUNCTIVE, EN_ATOMIC,
EN_MEMBER_SINGLE, EN_MEMBER_CHAIN, EN_MEMBER_NEGATIVE, EN_MEMBER_ATOMIC,
EN_CONDMEM_FUSED, EN_CONDMEM_DISJUNCTIVE, EN_CONDMEM_CHAIN, EN_CONDMEM_CONDITIONAL,
)
@ -406,8 +521,8 @@ def generate_problems(band: str, n: int) -> list[Problem]:
logical form for the reader-independent oracle cross-check.
"""
problems: list[Problem] = []
if band in _MEM_TEMPLATES:
templates = _MEM_TEMPLATES[band]
if band in _MEM_TEMPLATES or band in _CM_TEMPLATES:
templates = _MEM_TEMPLATES[band] if band in _MEM_TEMPLATES else _CM_TEMPLATES[band]
for i in range(n):
gold, builder, intended_premises, intended_query = templates[i % len(templates)]
problems.append(
@ -526,6 +641,9 @@ class DeductionSolver:
member = self._attempt_member(problem)
if member is not None:
return member
cond_member = self._attempt_cond_member(problem)
if cond_member is not None:
return cond_member
return _DeductionAttempt(
committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}",
case_id=problem.problem_id, shape=problem.class_name,
@ -562,6 +680,9 @@ class DeductionSolver:
member = self._attempt_member(problem)
if member is not None:
return member
cond_member = self._attempt_cond_member(problem)
if cond_member is not None:
return cond_member
return _DeductionAttempt(
committed=False, answer=None, reason="unprojectable",
case_id=problem.problem_id, shape=problem.class_name,
@ -597,6 +718,21 @@ class DeductionSolver:
case_id=problem.problem_id, shape=arg.band,
)
def _attempt_cond_member(self, problem: Problem) -> _DeductionAttempt | None:
"""Band v4-CM: the conditional-membership argument path, or ``None``
when the reader refuses (the caller then records the honest decline)."""
arg = read_cond_member_argument(problem.payload["text"])
if not isinstance(arg, CondMemberArgument):
return None
outcome = evaluate_entailment_with_trace(
arg.premise_formulas, arg.query_formula
).outcome
return _DeductionAttempt(
committed=outcome is not Entailment.REFUSED,
answer=_OUTCOME_TO_CLASS[outcome], reason="",
case_id=problem.problem_id, shape=arg.band,
)
@dataclass(frozen=True, slots=True)
class ConstructionGoldTether:

33
evals/deduction_serve/report.json
View file

@ -1,8 +1,8 @@
{
"aggregate": {
"correct": 80,
"correct": 106,
"declined": 0,
"n": 80,
"n": 106,
"wrong": 0
},
"all_correct": true,
@ -35,6 +35,27 @@
},
"n": 28
},
"v2_condmem": {
"all_cases_correct": true,
"by_gold": {
"declined": 7,
"entailed": 10,
"refuted": 4,
"unknown": 5
},
"correct_by_gold": {
"declined": 7,
"entailed": 10,
"refuted": 4,
"unknown": 5
},
"counts": {
"correct": 26,
"declined": 0,
"wrong": 0
},
"n": 26
},
"v2_en": {
"all_cases_correct": true,
"by_gold": {
@ -59,16 +80,16 @@
"v2_member": {
"all_cases_correct": true,
"by_gold": {
"declined": 7,
"declined": 6,
"entailed": 12,
"refuted": 3,
"unknown": 4
"unknown": 5
},
"correct_by_gold": {
"declined": 7,
"declined": 6,
"entailed": 12,
"refuted": 3,
"unknown": 4
"unknown": 5
},
"counts": {
"correct": 26,

17
evals/deduction_serve/runner.py
View file

@ -45,6 +45,7 @@ from chat.deduction_surface import looks_like_deductive_argument
from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism
from generate.meaning_graph.reader import Comprehension, comprehend
from generate.proof_chain.categorical import CategoricalError, decide_syllogism
from generate.proof_chain.cond_member import CondMemberArgument, read_cond_member_argument
from generate.proof_chain.english import EnglishArgument, read_english_argument
from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
from generate.proof_chain.member import MemberArgument, read_member_argument
@ -61,6 +62,10 @@ _SPLITS: tuple[tuple[str, Path], ...] = (
# same content-disjoint discipline (incl. the number-link table on real
# nouns: men, people, children, canaries, sheep).
("v2_member", _ROOT / "v2_member" / "cases.jsonl"),
# Band v4-CM (ADR-0259) — hand-authored conditional-membership arguments,
# same content-disjoint discipline (connectives composed over singular-
# membership clauses, incl. universal+connective fusion cases).
("v2_condmem", _ROOT / "v2_condmem" / "cases.jsonl"),
)
_OUTCOME_TO_CLASS = {
@ -124,9 +129,19 @@ def _decide_english(text: str) -> str:
def _decide_member(text: str) -> str:
"""Band v3-MEM fallback (ADR-0258) — mirrors ``_member_band_surface``."""
"""Band v3-MEM fallback (ADR-0258) — mirrors ``_member_band_surface``;
chains into the Band v4-CM fallback exactly as the composer does."""
arg = read_member_argument(text)
if not isinstance(arg, MemberArgument):
return _decide_cond_member(text)
outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome
return _OUTCOME_TO_CLASS[outcome]
def _decide_cond_member(text: str) -> str:
"""Band v4-CM fallback (ADR-0259) — mirrors ``_cond_member_band_surface``."""
arg = read_cond_member_argument(text)
if not isinstance(arg, CondMemberArgument):
return "declined"
outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome
return _OUTCOME_TO_CLASS[outcome]

26
evals/deduction_serve/v2_condmem/cases.jsonl Normal file
View file

@ -0,0 +1,26 @@
{"id": "ds-cm-0001", "text": "If Socrates is a man then Socrates is mortal. Socrates is a man. Therefore Socrates is mortal.", "gold": "entailed", "class": "conditional_modus_ponens"}
{"id": "ds-cm-0002", "text": "If the museum is open then the ticket booth is staffed. The ticket booth is not staffed. Therefore the museum is not open.", "gold": "entailed", "class": "conditional_modus_tollens"}
{"id": "ds-cm-0003", "text": "Either the witness is lying or the suspect is guilty. The witness is not lying. Therefore the suspect is guilty.", "gold": "entailed", "class": "either_disjunctive_syllogism"}
{"id": "ds-cm-0004", "text": "The key is in the drawer or the key is on the hook. The key is not in the drawer. Therefore the key is on the hook.", "gold": "entailed", "class": "plain_or_disjunctive_syllogism"}
{"id": "ds-cm-0005", "text": "If the alarm is triggered then the guard is alerted. If the sensor is triggered then the guard is alerted. The alarm is triggered or the sensor is triggered. Therefore the guard is alerted.", "gold": "entailed", "class": "constructive_dilemma"}
{"id": "ds-cm-0006", "text": "If the pressure is high then the valve is open. If the valve is open then the tank is draining. The pressure is high. Therefore the tank is draining.", "gold": "entailed", "class": "two_hop_chain"}
{"id": "ds-cm-0007", "text": "If Nova is a suspect then Nova is a person of interest. If Nova is a person of interest then Nova is a flight risk. Nova is a suspect. Therefore Nova is a flight risk.", "gold": "entailed", "class": "two_hop_chain_membership"}
{"id": "ds-cm-0008", "text": "All engineers are employees. If Dax is an employee then Dax is insured. Dax is an engineer. Therefore Dax is insured.", "gold": "entailed", "class": "universal_connective_fusion"}
{"id": "ds-cm-0009", "text": "If Dax is an employee then Dax is insured. All contractors are employees. Dax is a contractor. Therefore Dax is insured.", "gold": "entailed", "class": "fusion_reversed_order"}
{"id": "ds-cm-0010", "text": "All students are learners. Priya is a student. If Priya is a learner then Priya is curious. Therefore Priya is curious.", "gold": "entailed", "class": "fusion_universal_first_order"}
{"id": "ds-cm-0011", "text": "If the reactor is critical then the reactor is unstable. The reactor is critical. Therefore the reactor is not unstable.", "gold": "refuted", "class": "conditional_direct_contradiction"}
{"id": "ds-cm-0012", "text": "If the code compiles then the code is buildable. If the code is buildable then the code is deployable. The code compiles. Therefore the code is not deployable.", "gold": "refuted", "class": "chain_contradiction"}
{"id": "ds-cm-0013", "text": "All interns are trainees. If Kai is a trainee then Kai is supervised. Kai is an intern. Therefore Kai is not supervised.", "gold": "refuted", "class": "fusion_chain_contradiction"}
{"id": "ds-cm-0014", "text": "The switch is on or the switch is off. The switch is not on. Therefore the switch is not off.", "gold": "refuted", "class": "disjunct_elimination_denial"}
{"id": "ds-cm-0015", "text": "If it is raining then the ground is wet. The ground is wet. Therefore it is raining.", "gold": "unknown", "class": "affirming_the_consequent"}
{"id": "ds-cm-0016", "text": "If the server is overloaded then the response is slow. The server is not overloaded. Therefore the response is not slow.", "gold": "unknown", "class": "denying_the_antecedent"}
{"id": "ds-cm-0017", "text": "If the bridge is closed then the traffic is rerouted. Therefore the bridge is closed.", "gold": "unknown", "class": "no_anchor"}
{"id": "ds-cm-0018", "text": "The door is locked or the door is unlocked. Therefore the door is locked.", "gold": "unknown", "class": "bare_disjunction"}
{"id": "ds-cm-0019", "text": "All senators are legislators. If Elio is a legislator then Elio is a committee member. Priya is a senator. Therefore Elio is a committee member.", "gold": "unknown", "class": "fusion_wrong_individual"}
{"id": "ds-cm-0020", "text": "If the door is open then if the window is open then the room is cold. Therefore the room is cold.", "gold": "declined", "class": "nested_conditional"}
{"id": "ds-cm-0021", "text": "The car is red and the car is fast or the car is loud. Therefore the car is fast.", "gold": "declined", "class": "ambiguous_and_or"}
{"id": "ds-cm-0022", "text": "If Nora is a pilot then Nora is licensed. Nora is a pilot. Therefore Nora is licensed and Nora is trained.", "gold": "declined", "class": "compound_conclusion_out_of_band"}
{"id": "ds-cm-0023", "text": "If someone is a suspect then someone is questioned. Therefore someone is questioned.", "gold": "declined", "class": "quantifier_out_of_band"}
{"id": "ds-cm-0024", "text": "If Elio is a manager then dogs are loyal. Elio is a manager. Therefore dogs are loyal.", "gold": "declined", "class": "bare_plural_out_of_band"}
{"id": "ds-cm-0025", "text": "If Elio is a manager then Elio is the boss. Elio is a manager. Therefore Elio is the boss.", "gold": "declined", "class": "definite_description_out_of_band"}
{"id": "ds-cm-0026", "text": "If Elio is a manager then the car that speeds is dangerous. Elio is a manager. Therefore the car that speeds is dangerous.", "gold": "declined", "class": "relative_clause_out_of_band"}

2
evals/deduction_serve/v2_member/cases.jsonl
View file

@ -21,6 +21,6 @@
{"id": "ds-mem-0021", "text": "Dogs are loyal. Rex is a dog. Therefore Rex is loyal.", "gold": "declined", "class": "bare_plural_out_of_band"}
{"id": "ds-mem-0022", "text": "Socrates is the philosopher. All philosophers are wise. Therefore Socrates is wise.", "gold": "declined", "class": "definite_description_out_of_band"}
{"id": "ds-mem-0023", "text": "Socrates is a man. All men are mortal. Therefore all men are mortal.", "gold": "declined", "class": "universal_conclusion_out_of_band"}
{"id": "ds-mem-0024", "text": "If Socrates is a man then Socrates is mortal. Therefore Socrates is mortal.", "gold": "declined", "class": "mixed_structure_out_of_band"}
{"id": "ds-mem-0024", "text": "If Socrates is a man then Socrates is mortal. Therefore Socrates is mortal.", "gold": "unknown", "class": "conditional_no_anchor_formerly_out_of_band"}
{"id": "ds-mem-0025", "text": "Rex is a dog that barks. All dogs are loyal. Therefore Rex is loyal.", "gold": "declined", "class": "relative_clause_out_of_band"}
{"id": "ds-mem-0026", "text": "Socrates was a man. All men are mortal. Therefore Socrates is mortal.", "gold": "declined", "class": "tense_out_of_band"}

447
generate/proof_chain/cond_member.py Normal file
View file

@ -0,0 +1,447 @@
"""Conditional-membership argument reader — Band v4-CM (ADR-0259).
Composes Band v2-EN's connective grammar (``if/then``, ``or``, ``and``,
``either`` sugar) with Band v3-MEM's singular-membership sentence reading, so
"If Socrates is a man then Socrates is mortal. Socrates is a man. Therefore
Socrates is mortal." decides — the ``mixed_structure_out_of_band`` gap
ADR-0258 §6.1 reserved as a future band.
Why this needs no new negation layer (unlike v2-EN): v2-EN's leaf minter
(``_AtomTable.mint``) is negation-BLIND, so its grammar must strip "not"
before minting. This band's leaf is ``generate.proof_chain.member``'s own
``_parse_singular`` — already negation-aware (leading "not", the sentential
"it is not the case that" prefix, and copular "is not") — so a leaf is parsed
directly, no separate negation-extraction step.
Why composing is sound (ADR-0259 §3, the load-bearing argument): every
connective built here (``&``, ``|``, ``->``) is standard propositional
structure the ROBDD engine already decides; every leaf is a v3-MEM singular
fact minted and linked by the SAME closed morphology relation ADR-0258 §3
proved sound and (for this fragment) complete. A bare universal may now
instantiate at an individual named only inside a connective's leaf — still
sound, since ADR-0258 §3's argument does not depend on WHERE a named
individual appears — and a connective's leaf atom may unify with an atom a
universal's instantiation also produced (the fusion this band is named for).
UNKNOWN is rendered by the UNCHANGED ``render_entailment_member`` (ADR-0258):
its scoping ("reading each name as one individual and each class word at
face value…") is exactly as accurate here, since every clause is read all
the way to individual+class — connectives add no new hidden structure.
Dispatch order is load-bearing: a sentence is checked for a connective token
BEFORE the universal-lead check (not after), so a connective token can never
silently leak into an opaque universal/singular name or class run.
Tried strictly AFTER Bands v1 / v1b / v2-EN / v3-MEM (a fallback tier) — pure
widening; every previously-served argument is served byte-identically.
Refusal-first, closed reason vocabulary:
``empty``, ``question_sentence``, ``no_conclusion``,
``multiple_conclusions``, ``conclusion_not_last``, ``no_premises``,
``empty_side``, ``quantifier_out_of_band``, ``bare_plural_out_of_band``,
``definite_description_out_of_band``, ``relative_clause_out_of_band``,
``universal_conclusion_out_of_band``, ``compound_conclusion_out_of_band``,
``internal_negation_unread``, ``sentence_shape_out_of_band``,
``structural_leak``, ``nested_conditional``, ``ambiguous_and_or``,
``too_many_premises``, ``too_many_atoms``.
"""
from __future__ import annotations
from dataclasses import dataclass
# The v2-EN sentence splitter, tokenizer, and generic token-run splitter are
# reused VERBATIM (one normalization discipline across every argument band —
# deliberate private-name imports inside the proof_chain package, same
# precedent as generate.proof_chain.member).
from generate.proof_chain.english import _SENTENCE_RE, _split_on, _tokenize
from generate.proof_chain.member import (
_A_LEADS,
_E_LEAD,
_QUANTIFIER_TOKENS,
_Singular,
_Universal,
_forms_link,
_parse_singular,
_parse_universal,
)
from generate.proof_chain.member import _Reject as _MemberReject
from generate.proof_chain.shape import (
EN_CONDMEM_CHAIN,
EN_CONDMEM_CONDITIONAL,
EN_CONDMEM_DISJUNCTIVE,
EN_CONDMEM_FUSED,
)
#: Connective structure this band's grammar composes (v2-EN's inventory,
#: minus "therefore" — that token is the commit-gate handled by the
#: outer sentence loop, never part of a clause's own structure).
_CONNECTIVE_TOKENS = frozenset({"if", "then", "or", "and", "either"})
#: Honesty caps — beyond these the argument is refused, never truncated.
#: ``MAX_ATOMS`` counts minted (individual, class) pairs.
MAX_PREMISE_SENTENCES = 16
MAX_ATOMS = 24
@dataclass(frozen=True, slots=True)
class CondMemberArgument:
"""A successfully-read conditional-membership argument, engine-ready.
Same shape as ``MemberArgument``/``EnglishArgument``: ``premise_formulas``/
``query_formula`` are propositional formula strings over minted atom ids;
``atoms[i]`` displays the *(individual, class)* pair behind ``a{i}``.
``premise_texts``/``query_text`` are the normalized original sentences.
"""
premise_formulas: tuple[str, ...]
query_formula: str
premise_texts: tuple[str, ...]
query_text: str
band: str
atoms: tuple[str, ...]
@dataclass(frozen=True, slots=True)
class CondMemberRefusal:
"""A typed refusal — the argument is not honestly readable by this band."""
reason: str
detail: str = ""
class _Reject(Exception):
def __init__(self, reason: str, detail: str = "") -> None:
super().__init__(reason)
self.refusal = CondMemberRefusal(reason, detail)
# --- the formula tree: leaves are v3-MEM singular facts, not opaque atoms ----
@dataclass(frozen=True, slots=True)
class _Lit:
leaf: int
@dataclass(frozen=True, slots=True)
class _And:
left: "_Formula"
right: "_Formula"
@dataclass(frozen=True, slots=True)
class _Or:
left: "_Formula"
right: "_Formula"
@dataclass(frozen=True, slots=True)
class _Implies:
left: "_Formula"
right: "_Formula"
_Formula = _Lit | _And | _Or | _Implies
@dataclass(frozen=True, slots=True)
class _Connective:
"""A parsed connective sentence: its formula tree over LOCAL leaf indices,
plus the singular facts those indices reference (leaf-parse order)."""
formula: _Formula
leaves: tuple[_Singular, ...]
def _is_connective(toks: list[str]) -> bool:
return any(t in _CONNECTIVE_TOKENS for t in toks)
def _leaf(toks: list[str], leaves: list[_Singular], detail: str) -> _Lit:
"""One membership leaf — reuses v3-MEM's own singular parser verbatim,
which is already negation-aware and already guards every name/class run
(quantifiers, relative clauses, definite descriptions, tense, bare
plurals) via ``_check_run``."""
leaves.append(_parse_singular(toks, detail))
return _Lit(len(leaves) - 1)
def _parse_junction(toks: list[str], leaves: list[_Singular], detail: str) -> _Formula:
"""Or/and over membership leaves. "either" is consumed before a
disjunction; mixed top-level and+or refuses (English scope is genuinely
ambiguous); a conditional may not nest inside a junction."""
if "if" in toks or "then" in toks:
raise _Reject("nested_conditional", detail)
if toks and toks[0] == "either" and "or" in toks:
toks = toks[1:]
has_or = "or" in toks
has_and = "and" in toks
if has_or and has_and:
raise _Reject("ambiguous_and_or", detail)
if has_or or has_and:
sep = "or" if has_or else "and"
parts = _split_on(toks, sep)
if any(not p for p in parts):
raise _Reject("empty_side", detail)
combine = _Or if has_or else _And
node = _leaf(parts[0], leaves, detail)
for part in parts[1:]:
node = combine(node, _leaf(part, leaves, detail))
return node
return _leaf(toks, leaves, detail)
def _parse_node(toks: list[str], leaves: list[_Singular], detail: str) -> _Formula:
"""One full connective sentence: ``if <A> then <B>`` (junctions allowed on
both sides, no nested conditionals) or a bare junction."""
if toks and toks[0] == "if":
if "then" not in toks:
raise _Reject("nested_conditional", detail)
then_idx = toks.index("then")
antecedent = toks[1:then_idx]
consequent = toks[then_idx + 1 :]
if not antecedent or not consequent:
raise _Reject("empty_side", detail)
left = _parse_junction(antecedent, leaves, detail)
right = _parse_junction(consequent, leaves, detail)
return _Implies(left, right)
return _parse_junction(toks, leaves, detail)
def _parse_premise_records(
toks: list[str], detail: str
) -> list[_Singular | _Universal | _Connective]:
"""A premise sentence -> one or more records. A top-level conjunction
("<A> and <B>.", no "if"/"or" anywhere) splits into separate singular
records — identical to conjoining (v2-EN's exact discipline, ported).
Any OTHER connective-bearing sentence builds a ``_Connective``. A
connective-token check happens BEFORE the universal-lead check so a
stray connective token can never leak into a bare universal's name/class
run undetected."""
if toks[0] != "if" and "and" in toks and "or" not in toks and "if" not in toks:
parts = _split_on(toks, "and")
if any(not p for p in parts):
raise _Reject("empty_side", detail)
return [_parse_singular(p, detail) for p in parts]
if _is_connective(toks):
leaves: list[_Singular] = []
formula = _parse_node(toks, leaves, detail)
return [_Connective(formula, tuple(leaves))]
if toks[0] in _A_LEADS or toks[0] == _E_LEAD:
return [_parse_universal(toks, detail)]
if toks[0] in _QUANTIFIER_TOKENS:
raise _Reject("quantifier_out_of_band", detail)
return [_parse_singular(toks, detail)]
def _parse_conclusion(toks: list[str], detail: str) -> _Singular:
"""The conclusion stays a single singular fact (optionally negated) —
matching v3-MEM's own discipline; a universal or connective-shaped
conclusion refuses rather than attempting a compound render."""
if _is_connective(toks):
raise _Reject("compound_conclusion_out_of_band", detail)
if toks[0] in _A_LEADS or toks[0] == _E_LEAD:
raise _Reject("universal_conclusion_out_of_band", detail)
if toks[0] in _QUANTIFIER_TOKENS:
raise _Reject("quantifier_out_of_band", detail)
return _parse_singular(toks, detail)
def _contains_or(node: _Formula) -> bool:
if isinstance(node, _Lit):
return False
if isinstance(node, _Or):
return True
return _contains_or(node.left) or _contains_or(node.right)
def _count_implies(node: _Formula) -> int:
if isinstance(node, _Lit):
return 0
n = 1 if isinstance(node, _Implies) else 0
return n + _count_implies(node.left) + _count_implies(node.right)
def read_cond_member_argument(text: str) -> CondMemberArgument | CondMemberRefusal:
"""Read *text* as a conditional-membership argument, or refuse (typed).
Deterministic and pure: same text -> same ``CondMemberArgument``. The
conclusion is the final sentence, the sole "therefore"-led one, and must
be a single singular fact; every earlier sentence is a premise. Lowering
is two-pass exactly as v3-MEM's — sentences (and connective leaves) parse
first, THEN individuals/class-groups are collected from every singular
fact wherever it appears (bare, and-split, or nested inside a connective
tree), THEN atoms are minted and universals instantiate at every named
individual — with premise formulas emitted in sentence order.
"""
if not text or not text.strip():
return CondMemberRefusal("empty")
sentences = [
(m.group(1), m.group(2)) for m in _SENTENCE_RE.finditer(text) if m.group(1).strip()
]
if not sentences:
return CondMemberRefusal("empty")
premise_records: list[_Singular | _Universal | _Connective] = []
record_details: list[str] = []
premise_texts: list[str] = []
conclusion: _Singular | None = None
query_text: str | None = None
try:
for idx, (body, terminator) in enumerate(sentences):
if terminator == "?":
raise _Reject("question_sentence", body)
toks = _tokenize(body)
if not toks:
continue
if toks[0] == "therefore":
if conclusion is not None:
raise _Reject("multiple_conclusions", body)
if idx != len(sentences) - 1:
raise _Reject("conclusion_not_last", body)
rest = toks[1:]
if not rest:
raise _Reject("empty_side", body)
conclusion = _parse_conclusion(rest, body)
query_text = " ".join(rest)
continue
if len(premise_texts) >= MAX_PREMISE_SENTENCES:
raise _Reject("too_many_premises", body)
records = _parse_premise_records(toks, body)
premise_records.extend(records)
record_details.extend([body] * len(records))
premise_texts.append(" ".join(toks))
if conclusion is None or query_text is None:
return CondMemberRefusal("no_conclusion")
if not premise_records:
return CondMemberRefusal("no_premises")
# --- lowering (ADR-0259 §2): shared with v3-MEM's two-pass scheme --
all_records: list[_Singular | _Universal | _Connective] = [
*premise_records, conclusion,
]
# Named individuals, first-appearance order — scanning bare
# singulars AND every leaf nested inside a connective.
individuals: list[tuple[str, ...]] = []
def _visit_individual(ind: tuple[str, ...]) -> None:
if ind not in individuals:
individuals.append(ind)
for rec in all_records:
if isinstance(rec, _Singular):
_visit_individual(rec.ind)
elif isinstance(rec, _Connective):
for leaf in rec.leaves:
_visit_individual(leaf.ind)
# Class groups: each attested form joins the FIRST group whose
# representative it links to — greedy, deterministic, closed (the
# SAME morphology relation as v3-MEM).
group_of: dict[tuple[str, ...], int] = {}
reps: list[tuple[str, ...]] = []
def _register_form(form: tuple[str, ...]) -> None:
if form in group_of:
return
for gi, rep in enumerate(reps):
if _forms_link(form, rep):
group_of[form] = gi
return
group_of[form] = len(reps)
reps.append(form)
for rec in all_records:
if isinstance(rec, _Singular):
_register_form(rec.cls)
elif isinstance(rec, _Universal):
_register_form(rec.subject)
_register_form(rec.predicate)
elif isinstance(rec, _Connective):
for leaf in rec.leaves:
_register_form(leaf.cls)
mint: dict[tuple[int, int], str] = {}
atom_display: list[str] = []
def atom_for(ind_idx: int, group: int, detail: str) -> str:
key = (ind_idx, group)
if key not in mint:
if len(atom_display) >= MAX_ATOMS:
raise _Reject("too_many_atoms", detail)
mint[key] = f"a{len(atom_display)}"
atom_display.append(
f"{' '.join(individuals[ind_idx])} : {' '.join(reps[group])}"
)
return mint[key]
def atom_of_singular(fact: _Singular, detail: str) -> str:
atom = atom_for(individuals.index(fact.ind), group_of[fact.cls], detail)
return f"~({atom})" if fact.negated else atom
def render_formula(node: _Formula, leaves: tuple[_Singular, ...], detail: str) -> str:
if isinstance(node, _Lit):
return atom_of_singular(leaves[node.leaf], detail)
left = render_formula(node.left, leaves, detail)
right = render_formula(node.right, leaves, detail)
if isinstance(node, _And):
return f"({left}) & ({right})"
if isinstance(node, _Or):
return f"({left}) | ({right})"
return f"({left}) -> ({right})" # _Implies
premise_formulas: list[str] = []
for rec, detail in zip(premise_records, record_details):
if isinstance(rec, _Singular):
premise_formulas.append(atom_of_singular(rec, detail))
elif isinstance(rec, _Connective):
premise_formulas.append(render_formula(rec.formula, rec.leaves, detail))
else: # _Universal — instantiate at every named individual
for ind_idx in range(len(individuals)):
antecedent = atom_for(ind_idx, group_of[rec.subject], detail)
consequent = atom_for(ind_idx, group_of[rec.predicate], detail)
premise_formulas.append(
f"({antecedent}) -> (~({consequent}))"
if rec.negative
else f"({antecedent}) -> ({consequent})"
)
query_formula = atom_of_singular(conclusion, query_text)
except (_Reject, _MemberReject) as rej:
# ``_parse_singular``/``_parse_universal`` are v3-MEM's own functions,
# reused verbatim — their failures raise v3-MEM's OWN ``_Reject``
# class (same shape, different identity), so both are caught here and
# normalized to THIS band's refusal type.
return CondMemberRefusal(rej.refusal.reason, rej.refusal.detail)
connectives = [r for r in premise_records if isinstance(r, _Connective)]
has_universal = any(isinstance(r, _Universal) for r in premise_records)
if has_universal and connectives:
band = EN_CONDMEM_FUSED
elif any(_contains_or(c.formula) for c in connectives):
band = EN_CONDMEM_DISJUNCTIVE
elif sum(_count_implies(c.formula) for c in connectives) >= 2:
band = EN_CONDMEM_CHAIN
else:
band = EN_CONDMEM_CONDITIONAL
return CondMemberArgument(
premise_formulas=tuple(premise_formulas),
query_formula=query_formula,
premise_texts=tuple(premise_texts),
query_text=query_text,
band=band,
atoms=tuple(atom_display),
)
__all__ = [
"MAX_ATOMS",
"MAX_PREMISE_SENTENCES",
"CondMemberArgument",
"CondMemberRefusal",
"read_cond_member_argument",
]

27
generate/proof_chain/shape.py
View file

@ -77,8 +77,28 @@ EN_MEMBER_BANDS: tuple[str, ...] = (
EN_MEMBER_ATOMIC,
)
#: Band v4-CM (ADR-0259) — conditional-membership fusion arguments, composing
#: v2-EN's connective grammar with v3-MEM's singular-membership sentence
#: reading ("If Socrates is a man then Socrates is mortal. …"), read by
#: ``generate.proof_chain.cond_member``. Same ``en_`` license discipline: a
#: different reader must earn its own per-shape record. Priority order:
#: fused > disjunctive > chain > conditional.
EN_CONDMEM_FUSED = "en_condmem_fused"
EN_CONDMEM_DISJUNCTIVE = "en_condmem_disjunctive"
EN_CONDMEM_CHAIN = "en_condmem_chain"
EN_CONDMEM_CONDITIONAL = "en_condmem_conditional"
EN_CONDMEM_BANDS: tuple[str, ...] = (
EN_CONDMEM_FUSED,
EN_CONDMEM_DISJUNCTIVE,
EN_CONDMEM_CHAIN,
EN_CONDMEM_CONDITIONAL,
)
#: Every serving shape-band — the ratified ledger's full key set.
ALL_SHAPE_BANDS: tuple[str, ...] = SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS
ALL_SHAPE_BANDS: tuple[str, ...] = (
SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS + EN_CONDMEM_BANDS
)
def classify_deduction_shape(premises: tuple[str, ...], query: str) -> str:
@ -115,6 +135,11 @@ __all__ = [
"EN_ATOMIC",
"EN_CONDITIONAL_CHAIN",
"EN_CONDITIONAL_SINGLE",
"EN_CONDMEM_BANDS",
"EN_CONDMEM_CHAIN",
"EN_CONDMEM_CONDITIONAL",
"EN_CONDMEM_DISJUNCTIVE",
"EN_CONDMEM_FUSED",
"EN_DISJUNCTIVE",
"EN_MEMBER_ATOMIC",
"EN_MEMBER_BANDS",

2
scripts/verify_lane_shas.py
View file

@ -51,7 +51,7 @@ PINNED_SHAS: dict[str, str] = {
"public_demo": "7d8ba0dbae9287cfe0bf15d231fa78a75abc627121c14900439293e01e1cc1d3",
"math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4",
"deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f",
"deduction_serve_v1": "ec446d70a6ba2eaaf04671800924754a3cfaacfc46f3225ca73e961169cd625d",
"deduction_serve_v1": "b530ed99c414a6d1bdd239752b0e1c6c8c03893f402198def29122b9c2a8a8be",
}

301
tests/test_cond_member_argument_reader.py Normal file
View file

@ -0,0 +1,301 @@
"""Band v4-CM (ADR-0259) — conditional-membership argument reader contract.
The reader composes v2-EN's connective grammar (if/then, or, and, either)
with v3-MEM's singular-membership sentence reading over ONE shared
per-individual atom space. It is pure and deterministic. Soundness rides on
the ROBDD engine; these tests pin that the reader hands it the RIGHT problem
— in particular that a bare universal's instantiated atom correctly UNIFIES
with a connective leaf's atom when the two mechanisms share a class (the
"fusion" this band is named for).
"""
from __future__ import annotations
import pytest
from generate.proof_chain.cond_member import (
MAX_ATOMS,
MAX_PREMISE_SENTENCES,
CondMemberArgument,
CondMemberRefusal,
read_cond_member_argument,
)
from generate.proof_chain.member import MemberRefusal, read_member_argument
from generate.proof_chain.shape import (
EN_CONDMEM_CHAIN,
EN_CONDMEM_CONDITIONAL,
EN_CONDMEM_DISJUNCTIVE,
EN_CONDMEM_FUSED,
)
def _read(text: str) -> CondMemberArgument:
arg = read_cond_member_argument(text)
assert isinstance(arg, CondMemberArgument), arg
return arg
def _refusal(text: str) -> CondMemberRefusal:
ref = read_cond_member_argument(text)
assert isinstance(ref, CondMemberRefusal), ref
return ref
# --- the composition itself: what v3-MEM refuses, this band decides ----------
def test_the_gap_this_band_fills_is_real() -> None:
"""The exact ADR-0258 §6.1 scope-out: v3-MEM refuses this shape in
isolation (pinned in test_member_argument_reader.py); this band decides
it. Both facts hold at once — v3-MEM is unchanged, this is a new tier."""
text = "If Socrates is a man then Socrates is mortal. Socrates is a man. Therefore Socrates is mortal."
assert isinstance(read_member_argument(text), MemberRefusal)
assert isinstance(read_cond_member_argument(text), CondMemberArgument)
# --- the flagship reading -----------------------------------------------------
def test_flagship_socrates_reads_as_conditional_modus_ponens() -> None:
arg = _read(
"If Socrates is a man then Socrates is mortal. Socrates is a man. "
"Therefore Socrates is mortal."
)
assert arg.premise_formulas == ("(a0) -> (a1)", "a0")
assert arg.query_formula == "a1"
assert arg.premise_texts == (
"if socrates is a man then socrates is mortal", "socrates is a man",
)
assert arg.query_text == "socrates is mortal"
assert arg.band == EN_CONDMEM_CONDITIONAL
assert len(arg.atoms) == 2
def test_modus_tollens_over_membership_atoms() -> None:
arg = _read(
"If Socrates is a man then Socrates is mortal. Socrates is not mortal. "
"Therefore Socrates is not a man."
)
assert arg.premise_formulas == ("(a0) -> (a1)", "~(a1)")
assert arg.query_formula == "~(a0)"
def test_or_disjunctive_syllogism() -> None:
arg = _read(
"Socrates is a man or Socrates is a god. Socrates is not a god. "
"Therefore Socrates is a man."
)
assert arg.premise_formulas == ("(a0) | (a1)", "~(a1)")
assert arg.query_formula == "a0"
assert arg.band == EN_CONDMEM_DISJUNCTIVE
def test_either_spelling_disjunctive_syllogism() -> None:
arg = _read(
"Either Socrates is a man or Socrates is a god. Socrates is not a man. "
"Therefore Socrates is a god."
)
assert arg.premise_formulas == ("(a0) | (a1)", "~(a0)")
assert arg.query_formula == "a1"
def test_and_split_premise_is_two_bare_records_not_a_connective() -> None:
"""A top-level "X and Y" PREMISE (no if/or) splits into independent
singular records — identical to conjoining, mirroring v2-EN exactly —
rather than building an ``&`` formula."""
arg = _read(
"Socrates is a man and Plato is a man. All men are mortal. "
"Therefore Socrates is mortal."
)
# The universal instantiates at EVERY named individual (Socrates AND
# Plato), each producing its own freshly-minted consequent atom.
assert arg.premise_formulas == ("a0", "a1", "(a0) -> (a2)", "(a1) -> (a3)")
assert arg.query_formula == "a2"
assert arg.premise_texts == (
"socrates is a man and plato is a man", "all men are mortal",
)
def test_two_hop_chain() -> None:
arg = _read(
"If Socrates is a man then Socrates is a philosopher. "
"If Socrates is a philosopher then Socrates is wise. "
"Socrates is a man. Therefore Socrates is wise."
)
assert arg.premise_formulas == ("(a0) -> (a1)", "(a1) -> (a2)", "a0")
assert arg.query_formula == "a2"
assert arg.band == EN_CONDMEM_CHAIN
# --- the fusion mechanism: universal instantiation UNIFIES with a connective
# leaf's atom via the SAME closed morphology relation ------------------------
def test_universal_instantiation_unifies_with_connective_leaf() -> None:
"""The mechanism this band is named for: "all MEN are mortal" instantiates
Socrates : men -> Socrates : mortal via the SAME atom the connective's
consequent leaf mints for "Socrates is a man" (linked man<->men)."""
arg = _read(
"All men are mortal. If Socrates is a philosopher then Socrates is a man. "
"Socrates is a philosopher. Therefore Socrates is mortal."
)
assert arg.premise_formulas == ("(a0) -> (a1)", "(a2) -> (a0)", "a2")
assert arg.query_formula == "a1"
assert arg.band == EN_CONDMEM_FUSED
assert len(arg.atoms) == 3
def test_fusion_reversed_sentence_order_reads_identically() -> None:
arg = _read(
"If Socrates is a philosopher then Socrates is a man. All men are mortal. "
"Socrates is a philosopher. Therefore Socrates is mortal."
)
# The connective mints philosopher/man first (a0/a1); the universal's
# antecedent REUSES a1 (men links to man), minting only mortal fresh (a2).
assert arg.premise_formulas == ("(a0) -> (a1)", "(a1) -> (a2)", "a0")
assert arg.query_formula == "a2"
assert arg.band == EN_CONDMEM_FUSED
def test_fusion_does_not_leak_across_individuals() -> None:
"""Instantiating a bare universal for MULTIPLE named individuals must not
let one individual's fact force another's conclusion."""
arg = _read(
"All men are mortal. If Plato is a philosopher then Plato is a man. "
"Socrates is a man. Therefore Plato is mortal."
)
# mortal(plato) needs man(plato), which needs philosopher(plato) — never
# asserted; socrates's fact is irrelevant to the query.
from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome
assert outcome is Entailment.UNKNOWN
# --- band classification ------------------------------------------------------
@pytest.mark.parametrize(
("text", "band"),
[
(
"If Bo is a cat then Bo is quick. Bo is a cat. Therefore Bo is quick.",
EN_CONDMEM_CONDITIONAL,
),
(
"Bo is a cat or Bo is a dog. Bo is not a cat. Therefore Bo is a dog.",
EN_CONDMEM_DISJUNCTIVE,
),
(
"If Bo is a cat then Bo is a hunter. If Bo is a hunter then Bo is quick. "
"Bo is a cat. Therefore Bo is quick.",
EN_CONDMEM_CHAIN,
),
(
"All cats are hunters. If Bo is a stray then Bo is a cat. Bo is a stray. "
"Therefore Bo is a hunter.",
EN_CONDMEM_FUSED,
),
],
)
def test_band_classification(text: str, band: str) -> None:
assert _read(text).band == band
# --- typed refusals -----------------------------------------------------------
@pytest.mark.parametrize(
("text", "reason"),
[
(
"If the door is open then if the window is open then the room is cold. "
"Therefore the room is cold.",
"nested_conditional",
),
(
"The car is red and the car is fast or the car is loud. "
"Therefore the car is fast.",
"ambiguous_and_or",
),
(
"If Socrates is a man then Socrates is mortal. Socrates is a man. "
"Therefore Socrates is mortal and Socrates is wise.",
"compound_conclusion_out_of_band",
),
(
"Socrates is a man. Therefore all men are mortal.",
"universal_conclusion_out_of_band",
),
(
"If someone is a suspect then someone is questioned. "
"Therefore someone is questioned.",
"quantifier_out_of_band",
),
(
"If Socrates is a man then dogs are loyal. Socrates is a man. "
"Therefore dogs are loyal.",
"bare_plural_out_of_band",
),
(
"If Socrates is a man then Socrates is the philosopher. Socrates is a man. "
"Therefore Socrates is the philosopher.",
"definite_description_out_of_band",
),
(
"If Socrates is a man then the dog that barks is loud. Socrates is a man. "
"Therefore the dog that barks is loud.",
"relative_clause_out_of_band",
),
(
"If Socrates was a man then Socrates was mortal. Socrates is a man. "
"Therefore Socrates is mortal.",
"sentence_shape_out_of_band",
),
("Is Socrates a man? Therefore Socrates is mortal.", "question_sentence"),
(
"If Socrates is a man then Socrates is mortal. Socrates is a man.",
"no_conclusion",
),
("Therefore Socrates is mortal.", "no_premises"),
(
"If Socrates is a man then Socrates is mortal. "
"Therefore Socrates is mortal. Plato is a man.",
"conclusion_not_last",
),
("", "empty"),
],
)
def test_typed_refusals(text: str, reason: str) -> None:
assert _refusal(text).reason == reason
# --- honesty caps -------------------------------------------------------------
def test_premise_cap_refuses_not_truncates() -> None:
facts = " ".join(f"N{i} is a cat." for i in range(MAX_PREMISE_SENTENCES))
text = f"If Bo is a cat then Bo is quick. {facts} Therefore N0 is a cat."
ref = _refusal(text)
assert ref.reason == "too_many_premises"
def test_atom_cap_refuses_not_truncates() -> None:
n = MAX_ATOMS // 2 + 1
facts = " ".join(f"N{i} is a dog." for i in range(n))
ref = _refusal(
f"If Bo is a dog then Bo is loyal. {facts} All dogs are cats. "
f"Therefore N0 is a cat."
)
assert ref.reason == "too_many_atoms"
# --- determinism --------------------------------------------------------------
def test_reading_is_deterministic() -> None:
text = (
"All men are mortal. If Socrates is a philosopher then Socrates is a man. "
"Socrates is a philosopher. Therefore Socrates is mortal."
)
assert read_cond_member_argument(text) == read_cond_member_argument(text)

21
tests/test_deduction_serve_e2e.py
View file

@ -136,6 +136,27 @@ def test_member_argument_is_decided_end_to_end() -> None:
assert "Your premises entail: tweety is not a reptile" in negative.surface
def test_conditional_membership_fusion_is_decided_end_to_end() -> None:
"""The ADR-0259 flagship: a conditional whose clauses are membership
facts, decided through the real REPL spine — including the genuine
fusion case where a bare universal's instantiated atom unifies with a
connective leaf's atom."""
rt = _runtime(True)
resp = rt.chat(
"If Socrates is a man then Socrates is mortal. Socrates is a man. "
"Therefore Socrates is mortal."
)
assert resp.grounding_source == "deduction"
assert "Your premises entail: socrates is mortal" in resp.surface
fused = rt.chat(
"All men are mortal. If Socrates is a philosopher then Socrates is a man. "
"Socrates is a philosopher. Therefore Socrates is mortal."
)
assert fused.grounding_source == "deduction"
assert "Your premises entail: socrates is mortal" in fused.surface
def test_out_of_regime_argument_refuses_honestly() -> None:
"""A 'therefore' argument NO band can read (verb-phrase negation —
ADR-0257 scope-out #2, morphology work reserved for a future band) gets an

25
tests/test_deduction_serve_lane.py
View file

@ -14,6 +14,7 @@ from evals.deduction_serve.runner import _ROOT, _load, build_report
_V1 = _ROOT / "v1" / "cases.jsonl"
_V2_EN = _ROOT / "v2_en" / "cases.jsonl"
_V2_MEMBER = _ROOT / "v2_member" / "cases.jsonl"
_V2_CONDMEM = _ROOT / "v2_condmem" / "cases.jsonl"
def test_v1_lane_wrong_is_zero() -> None:
@ -56,7 +57,10 @@ def test_v2_member_lane_wrong_is_zero() -> None:
"""Band v3-MEM (ADR-0258): hand-authored membership/universal arguments —
real nouns exercising every number-link row-type (irregular, invariant,
each regular suffix rule) — decided with wrong=0 across all four verdicts
and seven distinct honest-decline shapes."""
and six distinct honest-decline shapes. (``ds-mem-0024``, a bare
conditional with no anchor, was promoted declined->unknown when Band
v4-CM landed — ADR-0259; it is genuinely UNKNOWN, not entailed, since the
antecedent is never asserted.)"""
report = build_report(_load(_V2_MEMBER))
assert report["n"] == 26
assert report["counts"]["wrong"] == 0
@ -64,7 +68,24 @@ def test_v2_member_lane_wrong_is_zero() -> None:
cbg = report["correct_by_gold"]
assert cbg.get("entailed", 0) >= 12
assert cbg.get("refuted", 0) >= 3
assert cbg.get("unknown", 0) >= 4
assert cbg.get("unknown", 0) >= 5
assert cbg.get("declined", 0) >= 6
def test_v2_condmem_lane_wrong_is_zero() -> None:
"""Band v4-CM (ADR-0259): hand-authored conditional-membership arguments
— v2-EN's connective grammar composed over v3-MEM's singular-membership
sentence reading, including genuine universal+connective fusion cases —
decided with wrong=0 across all four verdicts and seven distinct honest-
decline shapes."""
report = build_report(_load(_V2_CONDMEM))
assert report["n"] == 26
assert report["counts"]["wrong"] == 0
assert report["all_cases_correct"] is True
cbg = report["correct_by_gold"]
assert cbg.get("entailed", 0) >= 10
assert cbg.get("refuted", 0) >= 4
assert cbg.get("unknown", 0) >= 5
assert cbg.get("declined", 0) >= 7

60
tests/test_deduction_surface.py
View file

@ -231,6 +231,66 @@ def test_member_reader_refusal_keeps_prior_honest_surface() -> None:
assert "can't parse" in surface
def test_conditional_membership_fusion_is_decided_band_v4_cm() -> None:
"""The ADR-0258 §6.1 scope-out, now decided (ADR-0259): a conditional
whose clauses are membership facts, authoritatively (the
``en_condmem_conditional`` band holds an earned SERVE license)."""
surface = deduction_grounded_surface(
"If Socrates is a man then Socrates is mortal. Socrates is a man. "
"Therefore Socrates is mortal."
)
assert surface is not None
assert "Your premises entail: socrates is mortal" in surface
assert not surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE)
def test_conditional_membership_fusion_genuinely_fuses() -> None:
"""The mechanism this band adds: a bare universal's instantiated atom
unifies with a connective leaf's atom — neither mechanism alone decides
this argument."""
surface = deduction_grounded_surface(
"All men are mortal. If Socrates is a philosopher then Socrates is a man. "
"Socrates is a philosopher. Therefore Socrates is mortal."
)
assert surface is not None
assert "Your premises entail: socrates is mortal" in surface
def test_cond_member_unknown_is_scoped_to_the_instantiated_reading() -> None:
surface = deduction_grounded_surface(
"If Socrates is a man then Socrates is mortal. Therefore Socrates is mortal."
)
assert surface is not None
assert "Reading each name as one individual" in surface
assert "don't settle" in surface
def test_cond_member_unearned_band_would_be_hedged() -> None:
"""The en_condmem_* bands ride the SAME earned-license gate: strip the
license and the same sound answer is served DISCLOSED, never
authoritatively."""
surface = deduction_grounded_surface(
"If Socrates is a man then Socrates is mortal. Socrates is a man. "
"Therefore Socrates is mortal.",
license_lookup=lambda band: None,
)
assert surface is not None
assert surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE)
assert "Your premises entail: socrates is mortal" in surface
def test_cond_member_reader_refusal_keeps_prior_honest_surface() -> None:
"""When the conditional-membership band ALSO cannot read the argument
(here: a conditional nested inside another), the pre-existing honest
surface is preserved verbatim — the band only widens."""
surface = deduction_grounded_surface(
"If the door is open then if the window is open then the room is cold. "
"Therefore the room is cold."
)
assert surface is not None
assert "can't parse" in surface
def test_surface_is_deterministic() -> None:
text = "If p then q. p. Therefore q."
assert deduction_grounded_surface(text) == deduction_grounded_surface(text)