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

Add proof-chain corpus fixtures

Browse source
This commit is contained in:
Shay 2026-06-02 19:26:46 -07:00
parent 6ee6bb7915
commit 15307ca1f3
3 changed files with 1023 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

229
docs/research/robdd_proof_chain_design_note.md Normal file
View file

@ -0,0 +1,229 @@
# ROBDD Proof-Chain Design Note
**Status:** research note; reconciled with ADR-0201 / ADR-0202
**Scope:** propositional canonicalizer and proof-corpus design support
**Date:** 2026-06-02
This note is syntax-independent at the proof-corpus level, but the formula
grammar and atom contract are now fixed by ADR-0202. The canonicalizer internals
and canonical-key string are fixed by ADR-0201. Proof-chain DAG wiring and
inference-rule result objects remain future work.
## Executive Shape
Reduced ordered binary decision diagrams (ROBDDs) are a good fit for the
propositional proof-chain keystone because they make the intrinsic space of a
proposition explicit: a Boolean function over a fixed ordered variable space.
Within that space, equivalence is structural identity, not a rewrite guess.
The honesty boundary is just as important: this applies to propositional logic
under a fixed variable ordering. It does not transfer to predicate logic,
quantifiers, ungrounded propositions, or proof graphs with circular dependency.
Those cases should refuse with typed reasons rather than approximate.
## Minimal Hand-Rolled Requirements
A minimal ROBDD manager needs these pieces:
- Two terminal leaves, `FALSE` and `TRUE`, represented by stable identities.
- Nonterminal nodes with `(variable, low, high)` where `low` is the branch for
the variable being false and `high` is the branch for true.
- A fixed variable order shared by every proposition compared in the same
equivalence domain.
- A `mk(variable, low, high)` constructor that is the only way to build
nonterminal nodes.
- A unique table keyed by `(variable, low_id, high_id)`.
- A computed cache keyed by `(operator, left_id, right_id)` for binary `apply`.
The reduction rules are the load-bearing laws:
1. Eliminate redundant tests: if `low == high`, return the child.
2. Merge isomorphic subgraphs: if another node has the same variable and
children, return the existing node identity.
When these are enforced by `mk` and the variable order is fixed, a shared ROBDD
manager gives a strong canonical form: two represented functions are equivalent
iff their reduced diagrams are isomorphic. ADR-0201 exposes that identity as a
byte-deterministic structural `canonical_key` string, with tautology serialized
as `T` and contradiction serialized as `F`.
## Apply Algorithm
The core construction operator is `apply(op, left, right)`.
At each recursive step:
1. Return from the computed cache if `(op, left, right)` was already solved.
2. Apply terminal identities when both inputs are leaves, and simple short-cuts
where the selected operator permits them.
3. Select the topmost variable among the two input roots under the fixed order.
4. Recur on the low cofactors and high cofactors for that variable.
5. Reconstruct through `mk(top_variable, low_result, high_result)`.
6. Cache and return the resulting node.
This is propagation through the Boolean function manifold, with `mk` as the
corrective conjugate that collapses redundant or duplicated structure on the way
back up. The resulting identity is not a syntactic normal form; it is the
reduced function itself, shared in the manager.
## Variable Ordering
Variable ordering is not a cosmetic choice. ROBDD size can vary sharply across
orders, and finding an optimal ordering is itself hard. CORE should therefore
treat ordering as a deterministic contract, not an optimization contest.
For the small proof-step regime, the simplest adequate policy is:
- derive the variable set from declared proposition atoms,
- reject ungrounded variables before construction,
- sort by the ADR-0202 atom id,
- freeze that order for all propositions in a comparison or proof step.
Alternative local heuristics can be considered later only if they remain
byte-deterministic and are replayed as part of the trace. ADR-0201 chooses the
simplest v1 policy: atoms appearing in the formula, sorted lexicographically.
The important constraint is that two propositions being compared must be built
in the same manager ordering. Different orders can represent the same Boolean
function with different graph identities, so ordering must be part of the
canonicalization domain.
## Budget and Blowup Guard
Bryant's original framing is the right discipline for CORE: many practical
Boolean functions compact well, but worst-case exponential growth remains real.
The canonicalizer should therefore have an explicit budget guard, not an
implicit timeout.
Candidate budget dimensions:
- maximum variable count,
- maximum created node count,
- maximum recursive `apply` calls,
- maximum computed-cache entries,
- maximum parse/AST depth before ROBDD construction,
- maximum proof-DAG node count for proof-chain validation.
When a bound trips, the result should be the ADR-0202 typed refusal
`canonicalization_budget_exceeded`. It should not return a partial
canonical key, fall back to CNF/DNF, stochastic sampling, truth-table truncation,
or syntactic equality. Refusal preserves `wrong == 0`; churning or guessing does
not.
The budget should be part of replay evidence. A refusal is only useful if the
trace can say which bound tripped and at what count. That lets future work tune
the construction boundary from evidence without changing the logical verdict of
any completed case.
## Complement Edges
Complement edges are optional for a first implementation. They can reduce memory
by encoding negation as a bit on an edge or pointer instead of constructing a
separate complemented graph. Mature packages use this technique, but it raises
implementation obligations:
- regularize node pointers before unique-table lookup,
- define whether external root identity includes a complement mark,
- apply De Morgan transformations carefully in internal constructors,
- keep serialization byte-stable despite pointer-like internal representation.
For CORE v1, plain nodes are easier to audit. Complement edges become attractive
only if node pressure is observed under replayable benchmark evidence.
## Library vs Hand-Rolled
ADR-0201 chose the hand-rolled path. The tradeoff remains useful context for why
that choice fits the proof-step regime.
### Mature Library Path
CUDD-style packages are battle-tested. They provide unique tables, computed
caches, garbage collection, complement edges, dynamic variable reordering, and a
large operation set. That is the strongest argument for using a mature library:
the difficult low-level machinery has already been exercised by verification
workloads.
The cost is that such a dependency is heavy relative to the proof-step target:
opaque memory management, platform/build friction, optional dynamic reordering,
pointer-level identities, and many features CORE does not need for a small,
deterministic propositional corridor. If node identity is the canonical key,
library behavior must be constrained enough that replay is byte-stable.
### Minimal Hand-Rolled Path
A hand-rolled ROBDD manager is more work, but the v1 surface is compact:
terminal leaves, `mk`, unique table, computed cache, fixed variable ordering,
and `apply` for `not`, `and`, `or`, `implies`, and equivalence checking.
This path fits CORE's character when the proposition regime is deliberately
small: inspectable, deterministic, local, and easy to refuse when budgets trip.
The risk is underestimating edge cases in hash-consing, ordering, cache
invalidity, serialization, or proof-DAG interaction. Those risks should be paid
down with an independent corpus and explicit refusal tests, not hidden by broad
fallbacks.
## Proof-Chain Boundary
ROBDD identity proves truth-functional equivalence. It does not, by itself,
prove that a submitted proof chain is valid. The proof-chain layer still needs
its own structural checks:
- every referenced dependency must exist and be grounded,
- the dependency graph must be acyclic,
- each inference rule must declare the propositions it consumes,
- the derived proposition must be checked by the canonicalizer under the same
variable-order domain,
- out-of-regime formulas must refuse before canonical-key comparison.
The first `modus_ponens` rule can be framed as a small entailment check:
dependencies contain an antecedent and a matching implication; the proposed
conclusion must match the implication's consequent in the ADR-0202 formula
representation. Future proof-chain wiring still needs to choose whether this is
implemented by syntactic pattern over parsed formula nodes, by ROBDD entailment,
or by a narrow rule object that delegates equivalence checks to the canonicalizer.
## Validation Corpus Consequences
The independent corpus should test behavior, not implementation internals. It
should therefore include:
- equivalence pairs that force real Boolean canonicalization rather than shallow
operand sorting,
- non-equivalence near misses that catch over-collapse,
- TRUE/FALSE terminal reductions,
- valid and invalid `modus_ponens` examples,
- circular proof-DAG refusal,
- quantified/predicate out-of-regime refusal,
- budget-exceeded refusal for a scalable family.
The corpus does not assert concrete node numbers. It asserts
equality/difference of `canonical_key`, typed terminal identity (`T` / `F`), and
typed refusals under the ADR-0202 atom and formula contract.
## Confirmed Contract Points
- Formula representation: ADR-0202 grammar over declared atom ids.
- Atom grounding: per-case atoms declare `gloss` and either
`binding.features` for intended ADR-0144/ADR-0143 FeatureBundle matching or
`binding: null` for schematic atoms.
- Variable ordering: lexicographic sorted atoms appearing in the formula.
- Canonical key: ADR-0201 byte-deterministic structural string; `T` and `F` for
terminal constants.
- Budget refusal: `canonicalization_budget_exceeded`.
- Complement edges: out of v1; ADR-0201 shipped a plain hand-rolled ROBDD.
- Still future proof-chain work: proof-DAG dependency object, circularity
checker, and concrete inference-rule result object.
## Sources
- Randal E. Bryant, "Graph-Based Algorithms for Boolean Function
Manipulation," IEEE Transactions on Computers, C-35:8, 1986.
https://doi.org/10.1109/TC.1986.1676819
- Randal E. Bryant, "Binary Decision Diagrams: An Algorithmic Basis for
Symbolic Model Checking," 2018 chapter draft.
https://www.cs.cmu.edu/~bryant/pubdir/hmc-bdd18.pdf
- Fabio Somenzi, CUDD Programmer's Manual, release 2.5.0.
https://www.cs.rice.edu/~lm30/RSynth/CUDD/cudd/doc/
- Seiichiro Tani, Kiyoharu Hamaguchi, and Shuzo Yajima, "The complexity of the
optimal variable ordering problems of shared binary decision diagrams,"
ISAAC 1993. https://doi.org/10.1007/3-540-57568-5_270

57
tests/fixtures/proof_chain/README.md vendored Normal file
View file

@ -0,0 +1,57 @@
# Proof-Chain Fixture Scaffold
**Status:** ADR-0202 grammar filled; not wired into the live suite
**Scope:** data-only fixture scaffold; not wired into the live test suite
This directory is the independent validation scaffold for the propositional
canonicalizer and first `modus_ponens` proof-chain rule. The formula grammar,
atom declaration shape, and atom-to-FeatureBundle binding convention are governed
by `docs/decisions/ADR-0202-proposition-representation-contract.md`.
The fixture inventory in `propositional_cases.json` records concrete formula
strings, per-case `atoms` blocks, expected behaviors, and rationale. It is ready
for a future proof-chain harness to wire, but it is intentionally not part of the
live test suite yet.
## Atom Bindings
Where a case atom maps to a recognizable fact, the atom records the intended
ADR-0144/ADR-0143 `FeatureBundle` binding as `binding.features`. The corpus does
not author `EpistemicNode.node_id`; that is assigned at recognition time.
Schematic budget atoms use `binding: null`.
## Validation Boundaries
The three `modus_ponens` cases are validated at entailment only. Their typed rule
reasons (`conclusion_mismatch` / `missing_implication`) are marked pending phase
2.3 / ADR-0205, when the rule checker lands.
The two out-of-regime cases assert `out_of_decidable_regime` and record that this
is the `LogicRegimeError` reason produced by merged main after ADR-0201.1.
## Required Categories
- `equivalent_key`: propositions that must reduce to identical canonical keys.
- `different_key`: near-miss propositions that must not collapse.
- `tautology_or_contradiction`: formulas that reduce to TRUE/FALSE leaves.
- `modus_ponens`: proof-chain admission and refusal examples.
- `acyclicity`: circular dependency refusal cases.
- `out_of_regime`: quantified or predicate input outside propositional logic.
- `budget`: scalable ROBDD blowup cases that must refuse when over budget.
## Interface Assumptions
- Formula grammar: ADR-0202 section 1.
- Atom declaration and FeatureBundle binding: ADR-0202 section 2.
- TRUE/FALSE leaf identity: `T` / `F`.
- Budget refusal reason: `canonicalization_budget_exceeded`.
- Proof-chain rule and DAG fields are fixture data only until `proof_chain`
lands.
## Non-Goals
- No runtime wiring.
- No second canonicalizer implementation.
- No CNF/DNF fallback expectations.
- No predicate-logic equivalence claim.
- No repo capability claim.

737
tests/fixtures/proof_chain/propositional_cases.json vendored Normal file
View file

@ -0,0 +1,737 @@
{
"status": "ready_to_wire_when_proof_chain_lands",
"contract": "docs/decisions/ADR-0202-proposition-representation-contract.md",
"canonicalizer_contract": "docs/decisions/ADR-0201-proposition-canonicalizer.md",
"not_wired_into_live_suite": true,
"contains_concrete_formula_strings": true,
"conformance_policy": {
"non_refusal_cases": "All formula strings use the ADR-0202 grammar; every referenced atom is declared; every atom has a gloss and either FeatureBundle features or binding null.",
"refusal_cases": "Refusal probes either conform structurally and expect a proof-chain refusal, or intentionally present rejected input outside the formula grammar with a typed refusal reason."
},
"cases": [
{
"id": "PC-EQ-001",
"category": "equivalent_key",
"slot": "conjunction_commutativity",
"expected": "provable",
"expected_behavior": "identical_canonical_key",
"rationale": "Equivalent Boolean functions must share ROBDD identity under the fixed variable ordering.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains & Q_ground_wet",
"formula_b": "Q_ground_wet & P_rains",
"expected_relation": "same"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-EQ-002",
"category": "equivalent_key",
"slot": "disjunction_commutativity",
"expected": "provable",
"expected_behavior": "identical_canonical_key",
"rationale": "Operand order must not affect function identity.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains | Q_ground_wet",
"formula_b": "Q_ground_wet | P_rains",
"expected_relation": "same"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-EQ-003",
"category": "equivalent_key",
"slot": "conjunction_associativity",
"expected": "provable",
"expected_behavior": "identical_canonical_key",
"rationale": "Tree shape must not leak into canonical identity.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
},
"R_traffic_slow": {
"gloss": "traffic is slow",
"binding": { "features": { "agent": "traffic", "relation": "is", "state": "slow" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "(P_rains & Q_ground_wet) & R_traffic_slow",
"formula_b": "P_rains & (Q_ground_wet & R_traffic_slow)",
"expected_relation": "same"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-EQ-004",
"category": "equivalent_key",
"slot": "double_negation",
"expected": "provable",
"expected_behavior": "identical_canonical_key",
"rationale": "Logical involution must collapse to the original function.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "~~P_rains",
"formula_b": "P_rains",
"expected_relation": "same"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-EQ-005",
"category": "equivalent_key",
"slot": "implication_expansion",
"expected": "provable",
"expected_behavior": "identical_canonical_key",
"rationale": "Implication and its propositional expansion must be the same function.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains -> Q_ground_wet",
"formula_b": "~P_rains | Q_ground_wet",
"expected_relation": "same"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-EQ-006",
"category": "equivalent_key",
"slot": "de_morgan_conjunction",
"expected": "provable",
"expected_behavior": "identical_canonical_key",
"rationale": "Negated conjunction and disjunction of negations must share identity.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "~(P_rains & Q_ground_wet)",
"formula_b": "~P_rains | ~Q_ground_wet",
"expected_relation": "same"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-EQ-007",
"category": "equivalent_key",
"slot": "conjunction_distributes_over_disjunction",
"expected": "provable",
"expected_behavior": "identical_canonical_key",
"rationale": "Equivalent functions with different syntactic expansion must canonicalize together.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
},
"R_traffic_slow": {
"gloss": "traffic is slow",
"binding": { "features": { "agent": "traffic", "relation": "is", "state": "slow" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains & (Q_ground_wet | R_traffic_slow)",
"formula_b": "(P_rains & Q_ground_wet) | (P_rains & R_traffic_slow)",
"expected_relation": "same"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-EQ-008",
"category": "equivalent_key",
"slot": "disjunction_idempotence",
"expected": "provable",
"expected_behavior": "identical_canonical_key",
"rationale": "Duplicate operands must not create distinct Boolean identity.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains | P_rains",
"formula_b": "P_rains",
"expected_relation": "same"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-EQ-009",
"category": "equivalent_key",
"slot": "absorption",
"expected": "provable",
"expected_behavior": "identical_canonical_key",
"rationale": "Absorption catches syntactic normalizers that do not compute function identity.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains | (P_rains & Q_ground_wet)",
"formula_b": "P_rains",
"expected_relation": "same"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-NEQ-001",
"category": "different_key",
"slot": "implication_versus_converse_implication",
"expected": "not_provable",
"expected_behavior": "different_canonical_key",
"rationale": "Near-symmetric implications are not equivalent in general.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains -> Q_ground_wet",
"formula_b": "Q_ground_wet -> P_rains",
"expected_relation": "different"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-NEQ-002",
"category": "different_key",
"slot": "conjunction_versus_disjunction",
"expected": "not_provable",
"expected_behavior": "different_canonical_key",
"rationale": "The canonicalizer must not over-collapse common atoms.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains & Q_ground_wet",
"formula_b": "P_rains | Q_ground_wet",
"expected_relation": "different"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-NEQ-003",
"category": "different_key",
"slot": "grounded_atom_versus_negated_grounded_atom",
"expected": "not_provable",
"expected_behavior": "different_canonical_key",
"rationale": "Negation must change identity except for degenerate constants.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains",
"formula_b": "~P_rains",
"expected_relation": "different"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-NEQ-004",
"category": "different_key",
"slot": "strengthened_conjunction_versus_original_grounded_atom",
"expected": "not_provable",
"expected_behavior": "different_canonical_key",
"rationale": "Adding a premise changes the represented function.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"assertion": {
"kind": "canonical_key_relation",
"formula_a": "P_rains & Q_ground_wet",
"formula_b": "P_rains",
"expected_relation": "different"
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-TC-001",
"category": "tautology_or_contradiction",
"slot": "excluded_middle",
"expected": "provable",
"expected_behavior": "canonical_true_leaf",
"rationale": "A tautology must reduce to the TRUE terminal identity.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
}
},
"assertion": {
"kind": "terminal_key",
"formula": "P_rains | ~P_rains",
"expected_canonical_key": "T",
"expected_is_tautology": true,
"expected_is_contradiction": false
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-TC-002",
"category": "tautology_or_contradiction",
"slot": "contradiction",
"expected": "not_provable",
"expected_behavior": "canonical_false_leaf",
"rationale": "A contradiction must reduce to the FALSE terminal identity.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
}
},
"assertion": {
"kind": "terminal_key",
"formula": "P_rains & ~P_rains",
"expected_canonical_key": "F",
"expected_is_tautology": false,
"expected_is_contradiction": true
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-MP-001",
"category": "modus_ponens",
"slot": "valid_modus_ponens",
"expected": "provable",
"expected_behavior": "admit",
"rationale": "The first proof-chain rule should admit the canonical modus ponens form.",
"validation_scope": "validated at entailment only; typed rule-reasons pending phase 2.3 / ADR-0205",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"premises": ["P_rains -> Q_ground_wet", "P_rains"],
"conclusion": "Q_ground_wet",
"rule": "modus_ponens",
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-MP-002",
"category": "modus_ponens",
"slot": "invalid_modus_ponens_wrong_conclusion",
"expected": "refused",
"expected_behavior": "refuse",
"expected_refusal_reason": "conclusion_mismatch",
"validation_scope": "validated at entailment only; typed rule-reasons pending phase 2.3 / ADR-0205",
"rule_reason_status": "pending phase 2.3 / ADR-0205",
"rationale": "The rule must refuse a conclusion not entailed by the dependencies.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
},
"R_traffic_slow": {
"gloss": "traffic is slow",
"binding": { "features": { "agent": "traffic", "relation": "is", "state": "slow" } }
}
},
"premises": ["P_rains -> Q_ground_wet", "P_rains"],
"conclusion": "R_traffic_slow",
"rule": "modus_ponens",
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-MP-003",
"category": "modus_ponens",
"slot": "invalid_modus_ponens_missing_implication_premise",
"expected": "refused",
"expected_behavior": "refuse",
"expected_refusal_reason": "missing_implication",
"validation_scope": "validated at entailment only; typed rule-reasons pending phase 2.3 / ADR-0205",
"rule_reason_status": "pending phase 2.3 / ADR-0205",
"rationale": "The rule must refuse when the implication premise is missing.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"premises": ["P_rains"],
"conclusion": "Q_ground_wet",
"rule": "modus_ponens",
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-CYCLE-001",
"category": "acyclicity",
"slot": "two_node_dependency_cycle",
"expected": "refused",
"expected_behavior": "refuse",
"expected_refusal_reason": "circular_dependency",
"rationale": "Proof support must be a DAG; circular reasoning cannot prove the conclusion.",
"atoms": {
"P_rains": {
"gloss": "it is raining",
"binding": { "features": { "agent": "sky", "relation": "is", "state": "raining" } }
},
"Q_ground_wet": {
"gloss": "the ground is wet",
"binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } }
}
},
"proof_nodes": [
{ "id": "n1", "formula": "P_rains", "depends_on": ["n2"] },
{ "id": "n2", "formula": "Q_ground_wet", "depends_on": ["n1"] }
],
"conclusion_node": "n1",
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
},
{
"id": "PC-OOR-001",
"category": "out_of_regime",
"slot": "universally_quantified_predicate_statement",
"expected": "refused",
"expected_behavior": "refuse",
"expected_refusal_reason": "out_of_decidable_regime",
"rationale": "The propositional canonicalizer must not silently handle predicate logic.",
"atoms": {},
"rejected_input": "forall x. rains(x) -> wet(x)",
"main_output_verified": {
"exception": "LogicRegimeError",
"reason": "out_of_decidable_regime"
},
"conformance_checklist": {
"formula_grammar": false,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": false,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true,
"intentional_refusal_probe": true
}
},
{
"id": "PC-OOR-002",
"category": "out_of_regime",
"slot": "existentially_quantified_predicate_statement",
"expected": "refused",
"expected_behavior": "refuse",
"expected_refusal_reason": "out_of_decidable_regime",
"rationale": "Quantification is outside the propositional equivalence corridor.",
"atoms": {},
"rejected_input": "exists x. wet(x)",
"main_output_verified": {
"exception": "LogicRegimeError",
"reason": "out_of_decidable_regime"
},
"conformance_checklist": {
"formula_grammar": false,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": false,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true,
"intentional_refusal_probe": true
}
},
{
"id": "PC-BUDGET-001",
"category": "budget",
"slot": "scalable_robdd_pressure_family",
"expected": "refused",
"expected_behavior": "refuse_when_budget_exceeded",
"expected_refusal_reason": "canonicalization_budget_exceeded",
"rationale": "Large construction should refuse deterministically rather than churn or guess.",
"atoms": {
"X_b00": { "gloss": "schematic budget atom 00", "binding": null },
"X_b01": { "gloss": "schematic budget atom 01", "binding": null },
"X_b02": { "gloss": "schematic budget atom 02", "binding": null },
"X_b03": { "gloss": "schematic budget atom 03", "binding": null },
"X_b04": { "gloss": "schematic budget atom 04", "binding": null },
"X_b05": { "gloss": "schematic budget atom 05", "binding": null },
"X_b06": { "gloss": "schematic budget atom 06", "binding": null },
"X_b07": { "gloss": "schematic budget atom 07", "binding": null }
},
"assertion": {
"kind": "budget_refusal",
"formula": "X_b00 iff X_b01 iff X_b02 iff X_b03 iff X_b04 iff X_b05 iff X_b06 iff X_b07",
"max_nodes": 8
},
"conformance_checklist": {
"formula_grammar": true,
"all_formula_atoms_declared": true,
"atom_ids_stable_and_valid": true,
"all_atoms_have_gloss": true,
"bindings_are_features_or_null": true,
"no_quantifiers_predicates_or_functions": true,
"expected_outcome_allowed": true,
"equivalence_uses_canonical_key": true
}
}
]
}