feat: modus_ponens + disagreement rule — proof_chain wrong=0 mechanism (ADR-0205)
Phase 2.3: the first inference rule + the wrong=0 mechanism for proofs. - generate/proof_chain/rules.py: evaluate_modus_ponens / evaluate_proof_conclusion. Proof-layer dispatch (Option B) over proposition FORMULAS via the canonicalizer; never touches check_admissibility/_resolve_dep_units (proofs have no units). Disagreement rule = the select_self_verified twin: pool ALL admissible single-step MP derivations, require a unique canonical key == declared conclusion. Pooling (not filter-to-declared-first) is the soundness mechanism. - generate/logic_canonical.py: parse_top_implication (+ _unparse) — recovers an implication's syntactic antecedent/consequent (the ROBDD form doesn't preserve it). - Closed typed-reason set; the corpus's finer labels consolidate (6 disagreement refuse-labels -> conclusion_disagreement; 4 antecedent-flavor labels -> unestablished_antecedent — same redundancy, same mechanism-makes-one-distinction principle). - Honesty boundary (exact scope): guarantees a unique conclusion among SINGLE-STEP MP over the premises, NOT "uniquely entailed" by all strategies. Cross-check: all 24 GPT-5.5 adversarial corpus cases agree on OUTCOME against the real rule (no rule bug / no corpus outcome-misread); reasons consolidate as above. Mutation: filter-to-declared-first makes DISAGREE-007/010 wrongly admit -> pooling tests fail (pooling load-bearing). Drive-by fix (cleanup-as-you-find): merged ADR-0204 ProofNode.__post_init__ was dedented to module level -> all ProofNode validation was silently DEAD (smoke skips the dedicated test file; the smoke != full-suite hazard). Re-indented; validation restored. Additive (math lane untouched). Full binding-graph surface green; smoke 67.
This commit is contained in:
Shay
parent
0850e6fde7
commit
64f3da18a7
6 changed files with 453 additions and 26 deletions
116
docs/decisions/ADR-0205-modus-ponens-disagreement-rule.md
Normal file
116
docs/decisions/ADR-0205-modus-ponens-disagreement-rule.md
Normal file
|
|
@ -0,0 +1,116 @@
|
||||||
|
# ADR-0205 — modus_ponens + the Disagreement Rule (proof_chain's first inference rule)
|
||||||
|
|
||||||
|
**Status:** Accepted (proof_chain phase 2.3 — the first inference rule + the wrong=0 mechanism)
|
||||||
|
**Date:** 2026-06-02
|
||||||
|
**Relates to:** ADR-0204 (proof-graph builder — the proof-step shape this rule consumes),
|
||||||
|
ADR-0201/0201.1/0202 (canonicalizer + contract), ADR-0203 (acyclicity guard),
|
||||||
|
`generate.derivation.verify.select_self_verified` (the arithmetic twin of the disagreement rule).
|
||||||
|
**Deferred to:** ADR-0206 (atom→carrier grounding).
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## Context
|
||||||
|
|
||||||
|
proof_chain has a DAG substrate (ADR-0204) and a canonical form (ADR-0201). Phase
|
||||||
|
2.3 adds the first **inference rule** (`modus_ponens`) and the **wrong=0 mechanism
|
||||||
|
for proofs** (the disagreement/uniqueness rule). GPT-5.5 authored an independent
|
||||||
|
adversarial corpus (`modus_ponens_cases.json`, 24 cases: 6 valid / 8 invalid / 10
|
||||||
|
disagreement) against the ADR-0202 grammar, with the proof-step shape left
|
||||||
|
`[PENDING ADR-0204 SHAPE]` and the disagreement cases `[CONFIRM WITH OPUS]` — the
|
||||||
|
contract-first handshake.
|
||||||
|
|
||||||
|
## Decision
|
||||||
|
|
||||||
|
### 1. The MP-rule contract (committed before the rule)
|
||||||
|
|
||||||
|
- **Proof-step shape** = the already-landed ADR-0204 `Proof`/`ProofNode`
|
||||||
|
(`proof_from_premises` desugars premises→premise-nodes, conclusion→mp-node). The
|
||||||
|
`[PENDING ADR-0204 SHAPE]` placeholders resolve to this; the rule also accepts a
|
||||||
|
bare `(premises, conclusion)` for corpus cross-check.
|
||||||
|
- **Closed typed-reason set** (`generate/proof_chain/rules.py::MP_REASONS`):
|
||||||
|
`unique_canonical_conclusion` (admit); `missing_implication`,
|
||||||
|
`unestablished_antecedent`, `conclusion_mismatch`, `conclusion_disagreement` (refuse).
|
||||||
|
|
||||||
|
### 2. `evaluate_modus_ponens` — ROBDD-exact, bypassing unit-resolution
|
||||||
|
|
||||||
|
In `generate/proof_chain/rules.py` (the proof-layer dispatch, ADR-0205 Option B):
|
||||||
|
operates on proposition **formulas** via the canonicalizer; **never** calls
|
||||||
|
`check_admissibility` / `_resolve_dep_units` (proofs have no units — the named 2.2
|
||||||
|
constraint, satisfied by construction). An implication `A→B` fires iff `key(A)` is
|
||||||
|
an established premise key; the consequent `B` is recovered syntactically
|
||||||
|
(`logic_canonical.parse_top_implication`) because the ROBDD form does not preserve
|
||||||
|
which side is antecedent (`P→Q` and `¬P∨Q` share one diagram).
|
||||||
|
|
||||||
|
### 3. The disagreement / uniqueness rule (the wrong=0 mechanism)
|
||||||
|
|
||||||
|
The literal twin of `select_self_verified`: **pool ALL admissible single-step MP
|
||||||
|
derivations the premise set supports**, collect their canonical conclusion keys, and
|
||||||
|
admit iff they collapse to exactly one key equal to the declared conclusion;
|
||||||
|
≥2 distinct keys → refuse (`conclusion_disagreement`); one key ≠ declared →
|
||||||
|
`conclusion_mismatch`; no admissible derivation → `missing_implication` /
|
||||||
|
`unestablished_antecedent`.
|
||||||
|
|
||||||
|
**Pooling over the premise set — NOT filtering to the declared conclusion first —
|
||||||
|
is the soundness mechanism.** Filter-first would admit-by-assertion when the same
|
||||||
|
premises admit a different key (the `20/5 == 4` class one level up): e.g. a premise
|
||||||
|
set that MP-derives both an unrelated tautology and the declared atom, or both the
|
||||||
|
declared atom and a strictly stronger one. Collapse-vs-conflict is judged by **exact
|
||||||
|
canonical key**, never surface — equivalent paths (`P∧Q`/`Q∧P`, `Q→R`/`¬Q∨R`,
|
||||||
|
`Q`/`Q∧(R∨¬R)`) collapse and admit; subtly-different ones (`P∧Q`/`P∨Q`, `P→Q`/`Q→P`,
|
||||||
|
`Q`/`Q∧R`) refuse.
|
||||||
|
|
||||||
|
### 4. Reason-set consolidation (the reconciliation finding)
|
||||||
|
|
||||||
|
The mechanism makes one distinction per axis; the corpus's finer labels collapse onto
|
||||||
|
the closed set — *the same redundancy confirmed for the disagreement labels applies to
|
||||||
|
the invalid labels*:
|
||||||
|
|
||||||
|
- 6 disagreement refuse-labels (conflicting / contradictory / tautology_vs_substantive
|
||||||
|
/ distinct_atom / near_miss / stronger) → **`conclusion_disagreement`** (the rule
|
||||||
|
knows only: keys agree or they don't).
|
||||||
|
- 4 antecedent-flavor labels (missing_antecedent / antecedent_mismatch /
|
||||||
|
affirming_consequent / implication_direction_mismatch) → **`unestablished_antecedent`**
|
||||||
|
(the rule knows only: the available implication's antecedent is or isn't an
|
||||||
|
established premise; `affirming_consequent` and `implication_direction_mismatch` are
|
||||||
|
the identical pattern `A→B, conclusion≡A, premise≡B` — no mechanical distinction).
|
||||||
|
|
||||||
|
This consolidation is conveyed back to GPT-5.5 for the corpus's committed reasons.
|
||||||
|
|
||||||
|
## Honesty boundary (load-bearing — exact scope stated)
|
||||||
|
|
||||||
|
Through phase 2.3, proof_chain is **sound over its declared atoms**, not grounded in
|
||||||
|
recognized input (grounding is 2.4). And the disagreement rule's guarantee has a
|
||||||
|
**precise scope**: it guarantees a unique conclusion among **single-step modus ponens
|
||||||
|
derivations over the given premises** — **NOT** "uniquely entailed" by all proof
|
||||||
|
strategies (a stronger, currently-false claim). This must never be read as
|
||||||
|
"uniquely entailed." Same discipline as propositional-not-FOL.
|
||||||
|
|
||||||
|
## Evidence (cross-checked, not asserted)
|
||||||
|
|
||||||
|
- **All 24 corpus cases agree on OUTCOME against the real rule** (6 admit / 8 refuse
|
||||||
|
/ 4 admit / 6 refuse) — no rule bug, no corpus outcome-misread. Reasons: 3 exact,
|
||||||
|
21 consolidate onto the closed set as above.
|
||||||
|
- `tests/test_proof_chain_rules.py` — the 24 cases (transcribed, reproducible) + the
|
||||||
|
pooling guards. **Mutation:** a filter-to-declared-conclusion-first variant makes
|
||||||
|
MP-DISAGREE-007/010 wrongly admit → `test_pooling_*` fail. Pooling is load-bearing.
|
||||||
|
- **Drive-by fix (cleanup-as-you-find):** the merged ADR-0204 `ProofNode.__post_init__`
|
||||||
|
was dedented to module level, so **all `ProofNode` validation was silently dead**
|
||||||
|
(smoke skips the dedicated test file, so the merge missed it — the "smoke ≠ full
|
||||||
|
suite" hazard). Re-indented; validation restored;
|
||||||
|
`test_self_dependency_refused_at_proof_model` passes.
|
||||||
|
- Full binding-graph + admissibility surface green; smoke 67. Additive (no math path
|
||||||
|
touched).
|
||||||
|
|
||||||
|
## Three deferrals — settled
|
||||||
|
|
||||||
|
1. **modus_ponens bypasses unit-resolution** — by construction (proof-layer dispatch).
|
||||||
|
2. **Conclusion typing** — the rule needs the declared conclusion's key + premise
|
||||||
|
formulas, both reachable; `conclusion_symbol_id` suffices, **no `BoundUnknown`**.
|
||||||
|
3. **`semantic_role`** — proofs still not wired into serving; **stays `"unknown"`.**
|
||||||
|
|
||||||
|
## Deferred
|
||||||
|
|
||||||
|
- **2.4** — atom→ADR-0144 `EpistemicNode` grounding (ADR-0206). Until then, "sound
|
||||||
|
over declared atoms," never "reasons over input."
|
||||||
|
- Multi-step proof composition and a proof *search* (the disagreement rule here is
|
||||||
|
over a given premise set, single-step) — later, separately scoped.
|
||||||
|
|
@ -266,6 +266,41 @@ def _collect_atoms(ast: _Ast) -> set[str]:
|
||||||
return _collect_atoms(ast[1]) | _collect_atoms(ast[2])
|
return _collect_atoms(ast[1]) | _collect_atoms(ast[2])
|
||||||
|
|
||||||
|
|
||||||
|
_BINARY_OPS: Final[dict[str, str]] = {"and": "&", "or": "|", "implies": "->", "iff": "<->"}
|
||||||
|
|
||||||
|
|
||||||
|
def _unparse(ast: _Ast) -> str:
|
||||||
|
"""Render an AST back to a fully-parenthesized formula string. Used to hand a
|
||||||
|
sub-formula (e.g. an implication's antecedent/consequent) back to
|
||||||
|
:func:`canonicalize`. Parenthesized everywhere so re-parsing is unambiguous."""
|
||||||
|
kind = ast[0]
|
||||||
|
if kind == "atom":
|
||||||
|
return ast[1]
|
||||||
|
if kind == "const":
|
||||||
|
return "true" if ast[1] else "false"
|
||||||
|
if kind == "not":
|
||||||
|
return f"(~{_unparse(ast[1])})"
|
||||||
|
return f"({_unparse(ast[1])} {_BINARY_OPS[kind]} {_unparse(ast[2])})"
|
||||||
|
|
||||||
|
|
||||||
|
def parse_top_implication(formula: str) -> tuple[str, str] | None:
|
||||||
|
"""If ``formula``'s top-level connective is ``->``, return
|
||||||
|
``(antecedent, consequent)`` as formula strings; else ``None``.
|
||||||
|
|
||||||
|
Modus ponens needs the syntactic antecedent/consequent of an implication
|
||||||
|
premise — the ROBDD form does not preserve which side is which (``P->Q`` and
|
||||||
|
``~P|Q`` share one diagram), so this works at the parse layer. Raises
|
||||||
|
:class:`LogicError` / :class:`LogicRegimeError` on malformed / out-of-regime
|
||||||
|
input, consistent with :func:`canonicalize`."""
|
||||||
|
_reject_out_of_regime_text(formula)
|
||||||
|
tokens = _tokenize(formula)
|
||||||
|
_reject_out_of_regime_tokens(tokens)
|
||||||
|
ast = _Parser(tokens).parse()
|
||||||
|
if ast[0] == "implies":
|
||||||
|
return _unparse(ast[1]), _unparse(ast[2])
|
||||||
|
return None
|
||||||
|
|
||||||
|
|
||||||
# ---------------------------------------------------------------------------
|
# ---------------------------------------------------------------------------
|
||||||
# ROBDD manager (hand-rolled, minimal: mk + apply + negate + unique table)
|
# ROBDD manager (hand-rolled, minimal: mk + apply + negate + unique table)
|
||||||
# ---------------------------------------------------------------------------
|
# ---------------------------------------------------------------------------
|
||||||
|
|
|
||||||
|
|
@ -1,12 +1,14 @@
|
||||||
"""ADR-0204 — proof_chain: propositional proof graphs over the binding-graph DAG.
|
"""ADR-0204/0205 — proof_chain: propositional proof graphs over the binding-graph DAG.
|
||||||
|
|
||||||
Phase 2.2 (this module set): the proof-graph *builder* — proof → binding graph,
|
- Phase 2.2 (ADR-0204): the proof-graph *builder* — proof → binding graph, structure
|
||||||
structure only. The canonicalizer (`generate.logic_canonical`) and equivalence
|
only (`build_proof_graph`).
|
||||||
check (`generate.logic_equivalence`) it rides on are top-level modules; the
|
- Phase 2.3 (ADR-0205): the first inference rule + the wrong=0 mechanism —
|
||||||
inference rule (`modus_ponens` + the disagreement rule) is phase 2.3 / ADR-0205.
|
`evaluate_modus_ponens` / `evaluate_proof_conclusion` (modus_ponens + the
|
||||||
|
disagreement/uniqueness rule), in `rules.py`.
|
||||||
|
|
||||||
Honesty boundary (load-bearing through 2.3): sound over declared atoms, not
|
Honesty boundary (load-bearing through 2.3): sound over declared atoms, not grounded
|
||||||
grounded in recognized input.
|
in recognized input; the disagreement rule guarantees a unique conclusion among
|
||||||
|
SINGLE-STEP modus ponens over the premises, not "uniquely entailed" by all strategies.
|
||||||
"""
|
"""
|
||||||
|
|
||||||
from __future__ import annotations
|
from __future__ import annotations
|
||||||
|
|
@ -19,8 +21,26 @@ from .builder import (
|
||||||
build_proof_graph,
|
build_proof_graph,
|
||||||
)
|
)
|
||||||
from .model import Proof, ProofError, ProofNode, proof_from_premises
|
from .model import Proof, ProofError, ProofNode, proof_from_premises
|
||||||
|
from .rules import (
|
||||||
|
CONCLUSION_DISAGREEMENT,
|
||||||
|
CONCLUSION_MISMATCH,
|
||||||
|
MISSING_IMPLICATION,
|
||||||
|
MP_REASONS,
|
||||||
|
UNESTABLISHED_ANTECEDENT,
|
||||||
|
UNIQUE_CANONICAL_CONCLUSION,
|
||||||
|
MPOutcome,
|
||||||
|
MPVerdict,
|
||||||
|
evaluate_modus_ponens,
|
||||||
|
evaluate_proof_conclusion,
|
||||||
|
)
|
||||||
|
|
||||||
__all__ = (
|
__all__ = (
|
||||||
|
"CONCLUSION_DISAGREEMENT",
|
||||||
|
"CONCLUSION_MISMATCH",
|
||||||
|
"MISSING_IMPLICATION",
|
||||||
|
"MP_REASONS",
|
||||||
|
"MPOutcome",
|
||||||
|
"MPVerdict",
|
||||||
"PROOF_INTRODUCED_BY",
|
"PROOF_INTRODUCED_BY",
|
||||||
"PROOF_NO_UNIT",
|
"PROOF_NO_UNIT",
|
||||||
"PROOF_SOURCE_ID",
|
"PROOF_SOURCE_ID",
|
||||||
|
|
@ -28,6 +48,10 @@ __all__ = (
|
||||||
"ProofError",
|
"ProofError",
|
||||||
"ProofGraph",
|
"ProofGraph",
|
||||||
"ProofNode",
|
"ProofNode",
|
||||||
|
"UNESTABLISHED_ANTECEDENT",
|
||||||
|
"UNIQUE_CANONICAL_CONCLUSION",
|
||||||
"build_proof_graph",
|
"build_proof_graph",
|
||||||
|
"evaluate_modus_ponens",
|
||||||
|
"evaluate_proof_conclusion",
|
||||||
"proof_from_premises",
|
"proof_from_premises",
|
||||||
)
|
)
|
||||||
|
|
|
||||||
|
|
@ -37,26 +37,26 @@ class ProofNode:
|
||||||
depends_on: tuple[str, ...]
|
depends_on: tuple[str, ...]
|
||||||
rule: str
|
rule: str
|
||||||
|
|
||||||
def __post_init__(self) -> None:
|
def __post_init__(self) -> None:
|
||||||
object.__setattr__(self, "depends_on", tuple(self.depends_on))
|
object.__setattr__(self, "depends_on", tuple(self.depends_on))
|
||||||
|
|
||||||
if not isinstance(self.node_id, str) or not self.node_id.isidentifier():
|
if not isinstance(self.node_id, str) or not self.node_id.isidentifier():
|
||||||
raise ProofError(
|
raise ProofError(
|
||||||
"ProofNode.node_id must be a Python identifier str; "
|
"ProofNode.node_id must be a Python identifier str; "
|
||||||
f"got {self.node_id!r}"
|
f"got {self.node_id!r}"
|
||||||
)
|
)
|
||||||
if not isinstance(self.formula, str) or not self.formula.strip():
|
if not isinstance(self.formula, str) or not self.formula.strip():
|
||||||
raise ProofError("ProofNode.formula must be a non-empty str")
|
raise ProofError("ProofNode.formula must be a non-empty str")
|
||||||
if not isinstance(self.rule, str) or not self.rule.strip():
|
if not isinstance(self.rule, str) or not self.rule.strip():
|
||||||
raise ProofError("ProofNode.rule must be a non-empty str")
|
raise ProofError("ProofNode.rule must be a non-empty str")
|
||||||
if self.rule != self.rule.strip():
|
if self.rule != self.rule.strip():
|
||||||
raise ProofError("ProofNode.rule must not have leading/trailing whitespace")
|
raise ProofError("ProofNode.rule must not have leading/trailing whitespace")
|
||||||
if self.rule == "premise" and self.depends_on:
|
if self.rule == "premise" and self.depends_on:
|
||||||
raise ProofError('ProofNode.rule == "premise" requires empty depends_on')
|
raise ProofError('ProofNode.rule == "premise" requires empty depends_on')
|
||||||
if self.node_id in self.depends_on:
|
if self.node_id in self.depends_on:
|
||||||
# A self-dependency is a length-1 cycle; the binding-graph acyclicity
|
# A self-dependency is a length-1 cycle; the binding-graph acyclicity
|
||||||
# guard (ADR-0203) would also catch it, but refuse early and clearly.
|
# guard (ADR-0203) would also catch it, but refuse early and clearly.
|
||||||
raise ProofError(f"ProofNode {self.node_id!r} depends on itself")
|
raise ProofError(f"ProofNode {self.node_id!r} depends on itself")
|
||||||
|
|
||||||
|
|
||||||
@dataclass(frozen=True, slots=True)
|
@dataclass(frozen=True, slots=True)
|
||||||
|
|
|
||||||
127
generate/proof_chain/rules.py
Normal file
127
generate/proof_chain/rules.py
Normal file
|
|
@ -0,0 +1,127 @@
|
||||||
|
"""ADR-0205 — modus_ponens + the disagreement/uniqueness rule (proof_chain 2.3).
|
||||||
|
|
||||||
|
The first inference rule, and the wrong=0 mechanism for proofs. Operates on
|
||||||
|
proposition FORMULAS via the canonicalizer (`generate.logic_canonical`) — the
|
||||||
|
proof-layer dispatch (Option B): it never touches the math `check_admissibility` /
|
||||||
|
`_resolve_dep_units` (proofs have no units; the named 2.2 constraint, satisfied by
|
||||||
|
construction).
|
||||||
|
|
||||||
|
The disagreement rule is the literal twin of
|
||||||
|
`generate.derivation.verify.select_self_verified`: **pool ALL admissible single-step
|
||||||
|
MP derivations the premise set supports**, collect their canonical conclusion keys,
|
||||||
|
and admit iff they collapse to exactly one key equal to the declared conclusion.
|
||||||
|
Pooling over the premise set — NOT filtering to the declared conclusion first — is
|
||||||
|
the soundness mechanism: filter-first would admit-by-assertion when the same
|
||||||
|
premises admit a different key (the ``20/5 == 4`` class one level up).
|
||||||
|
|
||||||
|
**Honesty-boundary scope (load-bearing):** this guarantees a unique conclusion among
|
||||||
|
**single-step modus ponens** derivations over the given premises — NOT "uniquely
|
||||||
|
entailed" by all proof strategies. Same discipline as propositional-not-FOL.
|
||||||
|
|
||||||
|
Closed typed-reason set (the mechanism makes exactly these distinctions; the corpus's
|
||||||
|
finer labels collapse onto them — ADR-0205 §reason-set):
|
||||||
|
* 6 disagreement refuse-labels → ``conclusion_disagreement``;
|
||||||
|
* 4 antecedent-flavor labels (missing_antecedent / antecedent_mismatch /
|
||||||
|
affirming_consequent / implication_direction_mismatch) → ``unestablished_antecedent``.
|
||||||
|
"""
|
||||||
|
|
||||||
|
from __future__ import annotations
|
||||||
|
|
||||||
|
from dataclasses import dataclass
|
||||||
|
from enum import Enum
|
||||||
|
from typing import Final
|
||||||
|
|
||||||
|
from generate.logic_canonical import canonicalize, parse_top_implication
|
||||||
|
from generate.proof_chain.model import Proof, ProofError
|
||||||
|
|
||||||
|
|
||||||
|
class MPOutcome(str, Enum):
|
||||||
|
ADMIT = "admit"
|
||||||
|
REFUSE = "refuse"
|
||||||
|
|
||||||
|
|
||||||
|
# Closed reason vocabulary.
|
||||||
|
UNIQUE_CANONICAL_CONCLUSION: Final[str] = "unique_canonical_conclusion" # admit
|
||||||
|
MISSING_IMPLICATION: Final[str] = "missing_implication"
|
||||||
|
UNESTABLISHED_ANTECEDENT: Final[str] = "unestablished_antecedent"
|
||||||
|
CONCLUSION_MISMATCH: Final[str] = "conclusion_mismatch"
|
||||||
|
CONCLUSION_DISAGREEMENT: Final[str] = "conclusion_disagreement"
|
||||||
|
|
||||||
|
MP_REASONS: Final[frozenset[str]] = frozenset({
|
||||||
|
UNIQUE_CANONICAL_CONCLUSION,
|
||||||
|
MISSING_IMPLICATION,
|
||||||
|
UNESTABLISHED_ANTECEDENT,
|
||||||
|
CONCLUSION_MISMATCH,
|
||||||
|
CONCLUSION_DISAGREEMENT,
|
||||||
|
})
|
||||||
|
|
||||||
|
|
||||||
|
@dataclass(frozen=True, slots=True)
|
||||||
|
class MPVerdict:
|
||||||
|
outcome: MPOutcome
|
||||||
|
reason: str
|
||||||
|
conclusion_key: str | None # the unique admitted key (admit only)
|
||||||
|
derived_keys: tuple[str, ...] # distinct admissible-derivation keys (sorted)
|
||||||
|
|
||||||
|
|
||||||
|
def evaluate_modus_ponens(premises: tuple[str, ...], conclusion: str) -> MPVerdict:
|
||||||
|
"""Single-step modus ponens + the disagreement rule over ``premises``.
|
||||||
|
|
||||||
|
Admit iff the admissible single-step MP derivations the premises support
|
||||||
|
collapse to exactly one canonical key equal to ``conclusion``'s key. Refuses
|
||||||
|
(typed) otherwise. Propagates the canonicalizer's ``LogicError`` family on a
|
||||||
|
malformed / out-of-regime premise or conclusion."""
|
||||||
|
conclusion_key = canonicalize(conclusion).canonical_key
|
||||||
|
|
||||||
|
# Each premise establishes its own canonical key; implications also expose a
|
||||||
|
# syntactic (antecedent, consequent).
|
||||||
|
established: set[str] = set()
|
||||||
|
implications: list[tuple[str, str]] = []
|
||||||
|
for premise in premises:
|
||||||
|
established.add(canonicalize(premise).canonical_key)
|
||||||
|
parts = parse_top_implication(premise)
|
||||||
|
if parts is not None:
|
||||||
|
implications.append(parts)
|
||||||
|
|
||||||
|
if not implications:
|
||||||
|
return MPVerdict(MPOutcome.REFUSE, MISSING_IMPLICATION, None, ())
|
||||||
|
|
||||||
|
# Enumerate admissible derivations: an implication A->B fires iff key(A) is an
|
||||||
|
# established premise; it yields B. Pool over the WHOLE premise set.
|
||||||
|
derived: dict[str, None] = {} # insertion-ordered distinct yielded keys
|
||||||
|
for antecedent, consequent in implications:
|
||||||
|
if canonicalize(antecedent).canonical_key in established:
|
||||||
|
derived[canonicalize(consequent).canonical_key] = None
|
||||||
|
|
||||||
|
if not derived:
|
||||||
|
# Implication(s) present, but none has an established antecedent.
|
||||||
|
return MPVerdict(MPOutcome.REFUSE, UNESTABLISHED_ANTECEDENT, None, ())
|
||||||
|
|
||||||
|
distinct = tuple(sorted(derived))
|
||||||
|
if len(distinct) >= 2:
|
||||||
|
# The premises admit deriving distinct conclusions → disagreement.
|
||||||
|
return MPVerdict(MPOutcome.REFUSE, CONCLUSION_DISAGREEMENT, None, distinct)
|
||||||
|
|
||||||
|
only = distinct[0]
|
||||||
|
if only != conclusion_key:
|
||||||
|
# A single admissible derivation, but it concludes something else.
|
||||||
|
return MPVerdict(MPOutcome.REFUSE, CONCLUSION_MISMATCH, None, distinct)
|
||||||
|
|
||||||
|
return MPVerdict(MPOutcome.ADMIT, UNIQUE_CANONICAL_CONCLUSION, only, distinct)
|
||||||
|
|
||||||
|
|
||||||
|
def evaluate_proof_conclusion(proof: Proof) -> MPVerdict:
|
||||||
|
"""Evaluate ``proof``'s conclusion node as a modus_ponens step.
|
||||||
|
|
||||||
|
Wires the rule to the ADR-0204 ``Proof``: gathers the conclusion node's
|
||||||
|
dependency-node formulas as the premise set and evaluates. Requires the
|
||||||
|
conclusion node's ``rule == "modus_ponens"``."""
|
||||||
|
by_id = {n.node_id: n for n in proof.nodes}
|
||||||
|
concl = by_id[proof.conclusion_id]
|
||||||
|
if concl.rule != "modus_ponens":
|
||||||
|
raise ProofError(
|
||||||
|
f"evaluate_proof_conclusion expects a modus_ponens conclusion; "
|
||||||
|
f"got rule={concl.rule!r}"
|
||||||
|
)
|
||||||
|
premises = tuple(by_id[dep].formula for dep in concl.depends_on)
|
||||||
|
return evaluate_modus_ponens(premises, concl.formula)
|
||||||
125
tests/test_proof_chain_rules.py
Normal file
125
tests/test_proof_chain_rules.py
Normal file
|
|
@ -0,0 +1,125 @@
|
||||||
|
"""ADR-0205 — modus_ponens + disagreement rule (phase 2.3).
|
||||||
|
|
||||||
|
The 24 adversarial corpus cases (GPT-5.5's independent oracle) transcribed for a
|
||||||
|
committed, reproducible cross-check against the real rule: 6 valid / 8 invalid /
|
||||||
|
10 disagreement. The disagreement cases are the wrong=0 guard — 007/010 in
|
||||||
|
particular pin the pooling semantics: pool ALL admissible MP derivations and
|
||||||
|
require a unique key. A filter-to-declared-conclusion-first rule would admit them
|
||||||
|
(admit-by-assertion); pool-first refuses. That test failing under filter-first is
|
||||||
|
the proof the soundness mechanism is load-bearing.
|
||||||
|
"""
|
||||||
|
|
||||||
|
from __future__ import annotations
|
||||||
|
|
||||||
|
import pytest
|
||||||
|
|
||||||
|
from generate.proof_chain import (
|
||||||
|
CONCLUSION_DISAGREEMENT,
|
||||||
|
CONCLUSION_MISMATCH,
|
||||||
|
MISSING_IMPLICATION,
|
||||||
|
MP_REASONS,
|
||||||
|
Proof,
|
||||||
|
ProofNode,
|
||||||
|
UNESTABLISHED_ANTECEDENT,
|
||||||
|
UNIQUE_CANONICAL_CONCLUSION,
|
||||||
|
MPOutcome,
|
||||||
|
evaluate_modus_ponens,
|
||||||
|
evaluate_proof_conclusion,
|
||||||
|
)
|
||||||
|
|
||||||
|
# (id, premises, conclusion, expected_outcome, expected_reason) — reasons are the
|
||||||
|
# CLOSED set; the corpus's finer labels collapse onto them (ADR-0205 §reason-set).
|
||||||
|
CASES = [
|
||||||
|
# --- valid (admit) ---
|
||||||
|
("VALID-001", ("P", "P -> Q"), "Q", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
("VALID-002", ("P_rains", "P_rains -> Q_ground_wet"), "Q_ground_wet", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
("VALID-003", ("P and R", "(P and R) -> Q"), "Q", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
("VALID-004", ("P_switch_on", "P_switch_on -> (Q_lamp_lit or R_alarm_on)"), "Q_lamp_lit or R_alarm_on", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
("VALID-005", ("P", "P -> (Q -> R)"), "Q -> R", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
("VALID-006", ("(P or Q) and not R", "((P or Q) and not R) -> S"), "S", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
# --- invalid (refuse, typed) ---
|
||||||
|
("INVALID-001", ("P", "P -> Q"), "R", "refuse", CONCLUSION_MISMATCH),
|
||||||
|
("INVALID-002", ("P",), "Q", "refuse", MISSING_IMPLICATION),
|
||||||
|
("INVALID-003", ("Q", "P -> Q"), "P", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: affirming_consequent
|
||||||
|
("INVALID-004", ("R", "P -> Q"), "Q", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: antecedent_mismatch
|
||||||
|
("INVALID-005", ("P", "Q -> P"), "Q", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: implication_direction_mismatch
|
||||||
|
("INVALID-006", ("P", "(P or R) -> Q"), "Q", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: antecedent_mismatch
|
||||||
|
("INVALID-007", ("P", "P -> (Q or R)"), "Q", "refuse", CONCLUSION_MISMATCH),
|
||||||
|
("INVALID-008", ("P -> Q",), "Q", "refuse", UNESTABLISHED_ANTECEDENT), # corpus: missing_antecedent
|
||||||
|
# --- disagreement (admit: collapse to one key; refuse: distinct keys) ---
|
||||||
|
("DISAGREE-001", ("A", "A -> C", "B", "B -> C"), "C", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
("DISAGREE-002", ("A", "A -> (P and Q)", "B", "B -> (Q and P)"), "P and Q", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
("DISAGREE-003", ("A", "A -> (Q -> R)", "B", "B -> (not Q or R)"), "Q -> R", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
("DISAGREE-004", ("A", "A -> Q", "B", "B -> (Q and (R or not R))"), "Q", "admit", UNIQUE_CANONICAL_CONCLUSION),
|
||||||
|
("DISAGREE-005", ("A", "A -> (P and Q)", "B", "B -> (P or Q)"), "P and Q", "refuse", CONCLUSION_DISAGREEMENT),
|
||||||
|
("DISAGREE-006", ("A", "A -> Q_ground_wet", "B", "B -> Q_ground_damp"), "Q_ground_wet", "refuse", CONCLUSION_DISAGREEMENT),
|
||||||
|
("DISAGREE-007", ("A", "A -> (R or not R)", "B", "B -> Q"), "Q", "refuse", CONCLUSION_DISAGREEMENT),
|
||||||
|
("DISAGREE-008", ("A", "A -> Q", "B", "B -> not Q"), "Q", "refuse", CONCLUSION_DISAGREEMENT),
|
||||||
|
("DISAGREE-009", ("A", "A -> (P -> Q)", "B", "B -> (Q -> P)"), "P -> Q", "refuse", CONCLUSION_DISAGREEMENT),
|
||||||
|
("DISAGREE-010", ("A", "A -> Q", "B", "B -> (Q and R)"), "Q", "refuse", CONCLUSION_DISAGREEMENT),
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
@pytest.mark.parametrize("cid,premises,conclusion,outcome,reason", CASES, ids=[c[0] for c in CASES])
|
||||||
|
def test_corpus_case(cid, premises, conclusion, outcome, reason) -> None:
|
||||||
|
v = evaluate_modus_ponens(premises, conclusion)
|
||||||
|
assert v.outcome.value == outcome, cid
|
||||||
|
assert v.reason == reason, cid
|
||||||
|
assert v.reason in MP_REASONS
|
||||||
|
|
||||||
|
|
||||||
|
def test_admit_yields_the_canonical_conclusion_key() -> None:
|
||||||
|
from generate.logic_canonical import canonicalize
|
||||||
|
v = evaluate_modus_ponens(("P", "P -> Q"), "Q")
|
||||||
|
assert v.outcome is MPOutcome.ADMIT
|
||||||
|
assert v.conclusion_key == canonicalize("Q").canonical_key
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# The pooling semantics — the wrong=0 mechanism. 007/010 MUST refuse: the premises
|
||||||
|
# admit deriving a second distinct key, so pool-first refuses. A filter-first rule
|
||||||
|
# (keep only derivations whose key == declared conclusion, then check uniqueness)
|
||||||
|
# would admit both — admit-by-assertion. These assertions fail under that mutation.
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
def test_pooling_refuses_unrelated_tautology_path() -> None:
|
||||||
|
# 007: one path yields T (R or not R), the substantive path yields Q.
|
||||||
|
v = evaluate_modus_ponens(("A", "A -> (R or not R)", "B", "B -> Q"), "Q")
|
||||||
|
assert v.outcome is MPOutcome.REFUSE
|
||||||
|
assert v.reason == CONCLUSION_DISAGREEMENT
|
||||||
|
assert len(v.derived_keys) == 2 # T and key(Q) — distinct, pooled
|
||||||
|
|
||||||
|
|
||||||
|
def test_pooling_refuses_stronger_conclusion_path() -> None:
|
||||||
|
# 010: paths yield Q and (Q and R) — distinct keys.
|
||||||
|
v = evaluate_modus_ponens(("A", "A -> Q", "B", "B -> (Q and R)"), "Q")
|
||||||
|
assert v.outcome is MPOutcome.REFUSE
|
||||||
|
assert v.reason == CONCLUSION_DISAGREEMENT
|
||||||
|
assert len(v.derived_keys) == 2
|
||||||
|
|
||||||
|
|
||||||
|
def test_equivalent_paths_collapse_not_disagree() -> None:
|
||||||
|
# 003: Q->R and (not Q or R) are equivalent → one key → admit.
|
||||||
|
v = evaluate_modus_ponens(("A", "A -> (Q -> R)", "B", "B -> (not Q or R)"), "Q -> R")
|
||||||
|
assert v.outcome is MPOutcome.ADMIT
|
||||||
|
assert len(v.derived_keys) == 1
|
||||||
|
|
||||||
|
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
# Wiring to the ADR-0204 Proof.
|
||||||
|
# ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
def test_evaluate_proof_conclusion_via_builder_shape() -> None:
|
||||||
|
proof = Proof(
|
||||||
|
nodes=(
|
||||||
|
ProofNode("premise_0", "P", (), "premise"),
|
||||||
|
ProofNode("premise_1", "P -> Q", (), "premise"),
|
||||||
|
ProofNode("conclusion", "Q", ("premise_0", "premise_1"), "modus_ponens"),
|
||||||
|
),
|
||||||
|
conclusion_id="conclusion",
|
||||||
|
)
|
||||||
|
v = evaluate_proof_conclusion(proof)
|
||||||
|
assert v.outcome is MPOutcome.ADMIT
|
||||||
|
assert v.reason == UNIQUE_CANONICAL_CONCLUSION
|
||||||
Loading…
Reference in a new issue