Crate logicaffeine_proof

Expand description

§logicaffeine-proof

A backward-chaining proof engine over an owned, arena-independent IR (ProofExpr / ProofTerm): it searches for derivations, certifies them into kernel terms, and offers Socratic, leading-question hints when a proof gets stuck. It embodies the Curry-Howard correspondence — propositions are types, proofs are programs, verification is type checking.

Part of the Logicaffeine workspace. Tier 2 — depends on logicaffeine_base and logicaffeine_kernel. Liskov invariant: no dependency on the language crate, so the engine is reusable across front-ends.

§Role in the workspace

This crate owns proof representation, search, and certification — the trust core that both logicaffeine_language and logicaffeine_compile reach without a dependency cycle. The LogicExpr → ProofExpr lowering lives in the language crate, not here, so the proof engine stays pure and the Liskov boundary holds.

The single trust door: a proof is verified iff the chainer found a derivation, the certifier turned it into a kernel Term, and the kernel type-checked that term against the goal type. An externally built DerivationTree (e.g. from the grid solver) is re-checked the same way, so untrusted search sits outside the trusted base — a wrong tree yields verified == false, never a false claim. Trust tiers run fast → strong: untrusted CDCL/SMT (cnf::cdcl_entails, oracle) → RUP-certified (rup::entails_certified, sat::prove_unsat) → kernel-certified (verify). See proof-and-verification.md.

§Public API

Re-exported at the crate root: BackwardChainer, ProofError, suggest_hint, SocraticHint, SuggestedTactic, Substitution; plus ProofTerm, ProofExpr, MatchArm, InferenceRule, DerivationTree, ProofGoal defined directly in lib.rs.

Search — engine::BackwardChainer:

let mut prover = BackwardChainer::new();
prover.set_max_depth(depth: usize);
prover.add_axiom(expr: ProofExpr);
prover.knowledge_base() -> &[ProofExpr];
prover.prove(goal: ProofExpr) -> ProofResult<DerivationTree>;
prover.prove_with_goal(goal: ProofGoal) -> ProofResult<DerivationTree>;

The single door — verify:

verify::prove_certify_check(premises: &[ProofExpr], goal: &ProofExpr) -> VerifiedProof;
verify::prove_certify_check_bounded(premises, goal, max_depth: usize) -> VerifiedProof;
verify::check_derivation(premises, goal, tree: DerivationTree) -> VerifiedProof;
verify::detect_conflict(premises: &[ProofExpr]) -> ConflictReport;

VerifiedProof { derivation, proof_term, kernel_ctx, verified, verification_error } carries the re-checkable kernel term; detect_conflict returns a kernel proof of False plus the indices of the clashing premises.

IR — ProofTerm (Constant, Variable, Function, Group, BoundVarRef) and ProofExpr cover full FOL plus extensions: connectives, quantifiers, Modal / Counterfactual / Temporal / TemporalBinary, Lambda / App, Neo-Davidsonian NeoEvent, inductive Ctor / Match / Fixpoint / TypedVar, and unification Holes. InferenceRule names the move at each step — ModusPonens / ModusTollens, ∧/∨ intro & elim, ∀/∃ intro & elim, ModalAccess, StructuralInduction, Leibniz Rewrite, ArithDecision, ReductioAdAbsurdum, CaseAnalysis, DisjunctionCases, … A DerivationTree { conclusion, rule, premises, depth, substitution } is the prover’s result; ProofGoal { target, context } is consumed.

Hints — hints:

hints::suggest_hint(goal: &ProofExpr, kb: &[ProofExpr], failed: &[SuggestedTactic]) -> SocraticHint;

SocraticHint { text, suggested_tactic, priority } proposes a SuggestedTactic rather than giving the answer outright.

SAT / model checking (Z3-free, browser-ready) — sat and bmc:

sat::find_model(e: &ProofExpr) -> ModelOutcome;            // Sat(model) | Unsat | Unsupported
sat::prove_equivalence(a, b: &ProofExpr) -> EquivOutcome;  // Equivalent | Differ(cex) | Unsupported
sat::prove_unsat(e: &ProofExpr) -> UnsatOutcome;           // Refuted (RUP) | Sat(model) | Unsupported
bmc::find_counterexample(init, trans, property, max_k) -> BmcOutcome;
bmc::prove_invariant(init, trans, property, k) -> InductionOutcome;  // k-induction, unbounded
bmc::check_vacuity(antecedent: &ProofExpr) -> VacuityOutcome;

UNSAT verdicts from sat are independently RUP-certified (a refutation the trusted checker cannot replay yields Unsupported, never a false Refuted); bmc reduces BMC, k-induction, and vacuity to prove_unsat.

Other trust-core modules: certifier (Curry-Howard certify: DerivationTree → kernel Term), unify (Robinson unification + occurs check, capture-avoiding beta_reduce, Miller patterns), grounding (expand bounded quantifiers over a finite domain), grid_solver (certified logic-grid solver: watched-literal unit propagation + DPLL), cdcl (CDCL(T) core: 2-watched lits, 1-UIP, VSIDS, Luby, Theory trait, DRAT/LRAT log), cnf (Tseitin clausification), rup (RUP checker), arith (proof-producing integer-equality oracle), error (ProofError / ProofResult).

§Module atlas

Beyond the trust core, the crate is a broad library of certified reasoners and proof systems. Grouped by capability — every entry is a pub mod:

SAT/SMT engines & interchange — dimacs (DIMACS CNF I/O), satcli (the SAT command-line driver shared verbatim by the logos-sat binary and largo sat: competition output, certificate export, injected streams), twosat (2-SAT via implication-graph SCC), hornsat (Horn-SAT unit propagation), sdcl (Satisfaction-Driven Clause Learning), inprocess (certified inprocessing simplifications), discrimination (the first-order discrimination-tree index under simp).
Certified proof output & trust tiers — proof (shared proof-step vocabulary), proof_emit (DRAT/LRAT/DPR trace emission), proof_rewrite (proof-rewrite 2-cells), pr (propagation-redundancy checker), res_width (resolution-width lower bounds), complexity (self-sizing refutation bounds).
Algebraic proof systems — gf2 (GL(n,2)), xorsat / xor_engine / xor_drat (GF(2) parity: Gaussian XOR-SAT, DPLL(XOR), and the CNF→DRAT bridge), modp / polycalc_gfp (GF(p) linear algebra + Nullstellensatz), modm (ℤ/m by CRT), polycalc (Polynomial Calculus / Nullstellensatz over GF(2)), pseudo_boolean (cutting planes), affine / affine_gfp (the AGL(n,2) / AGL(n,p) affine symmetry a permutation break cannot see), sos (exact Sum-of-Squares / Positivstellensatz), lll (Lovász Local Lemma certificate).
Symmetry — symmetry / symmetry_detect (detection), sym_break (lex-leader breaking), sym_certify (certified breaking), sym_dynamic (Symmetric Explanation Learning), permgroup (Schreier–Sims BSGS — the non-abelian coset decision), orbit_stability (symmetric Nullstellensatz at every scale), families / census (parametric hard-instance generators + the small-n SAT-space census).
Combinatorial reasoners — pigeonhole / matching (bipartite-matching infeasibility), cardinality (cardinality constraints over boolean atoms), counting_principle (the modular counting principle Count_q(n): O(clauses) recognition, q ∤ n certificate), parity_cardinality (the coupled exactly-one + parity obstruction, decided by GF(2) augmentation), interval_sched (sweep-line scheduling), register_alloc (linear-scan allocation as a Hall reasoner), hypercube (Boolean-hypercube subcube cover), ordering (the GT(n) linear-ordering contradiction: polynomial-time recognizer + certified refuter for the no-maximum total order the general cascade only decides by super-polynomial search), lyapunov (Lyapunov-measure synthesis).
The ∞-tower (homotopy of SAT) — cubical (d-dimensional cubical homology), kan_complex / two_type / two_group (∞-groupoids had as objects), category_collapse / groupoid / coalgebra (the categorical meaning of symmetry breaking), eilenberg_maclane / postnikov / steenrod (K(A,n), k-invariants, the Steenrod algebra), progress_complex / trace_determinism (higher homotopy from real concurrency: determinism = contractibility).
Tactics, developments & simplification — tactic / tactic_script (interactive goal-state proving), formula (formal-FOL surface-text parser), development (## Theory block bodies), simp (oriented rewrite-rule sets).
Arithmetic, optimization & dispatch — linarith_solve (Fourier–Motzkin LIA core), optimize (certified SAT-based minimization), solve (the structure-detecting auto-dispatcher that fronts the whole arsenal), ait (certified algorithmic-information / description-length objects), isogeny (certified SIDH/SIKE torsion-image witnesses).
Number-theory / cryptanalysis substrate — factor (structural factoring: trial / Fermat / Pollard p−1 / rho + the RSA-ceiling thesis), elliptic (Montgomery x-only ECM), period (order-finding — the classical shell of Shor’s algorithm), lattice (exact LLL / Coppersmith over Rational), fp2 (𝔽_{p²} arithmetic + the supersingular 2-isogeny graph), hyperelliptic (genus-2 Richelot (2,2)-isogeny — the Castryck–Decru mechanism), cyclotomic (the power-of-two Module-LWE ring ℤ[X]/(Xⁿ+1)). Pure number theory over logicaffeine_base::numeric — the hardness lens isogeny / ait / solve ride on. (Relocated from logicaffeine_base in 0.10: the prover is their only consumer.)

§Feature flags

Flag	Effect
(default)	Kernel-certified search + SAT/RUP/BMC. No Z3, no external runtime dependency.
`verification`	Pulls in `logicaffeine-verify`, enabling `oracle` (Z3 SMT fallback) and the private `modal_translation` (modal/temporal → world-indexed FOL). Z3 verdicts are never kernel-certified.

§Tactics and decision procedures

Beyond the certified SAT/BMC core, the crate ships a tactic layer and algebraic solvers:

engine — the backward-chaining proof engine.
rule_search — aesop-style rule-set search, turning auto’s fixed cascade into a searchable rule database.
crush — the grind-style closer: E-matches quantified equality lemmas into the goal.
decide — proof by evaluation for closed decidable goals.
omega_solve — omega: linear integer (Presburger) arithmetic.
lemma_index — exact? / apply? premise selection over a named, certified lemma index.
counterexample — when a goal is false, exhibits a model instead of just failing.
gf — Galois-field (GF(2)/GF(p)) arithmetic backing the algebraic refutations.
polycalc_zm — Nullstellensatz over the rings ℤ/m (composite moduli, zero divisors and all).
cofactor — the cofactor-DAG lens: symmetry above the instance.

§Dependencies

Internal: logicaffeine-base, logicaffeine-kernel; logicaffeine-verify (optional, gated behind verification). No dependency on the language crate (Liskov invariant), and no external (non-workspace) crates — the default build is pure Rust with no Z3 and no runtime dependency, which is what keeps the SAT/BMC stack browser-ready.

§License

Business Source License 1.1 — see LICENSE.md.

Docs index · Root README · Changelog

Re-exports§

pub use engine::BackwardChainer;
pub use error::ProofError;
pub use hints::suggest_hint;
pub use hints::SocraticHint;
pub use hints::SuggestedTactic;
pub use unify::Substitution;

Modules§

affine: The affine group AGL(n,2) — the symmetry a permutation break cannot see.
affine_gfp: The affine group AGL(n,p) over GF(p) — the mod-p generalization of the affine break.
ait: Algorithmic information theory — certified description-length objects
arith: Proof-PRODUCING arithmetic oracle (untrusted search, kernel-checked proof).
bmc: Bounded model checking, k-induction, and vacuity over ProofExpr — pure-Rust, certified, Z3-free, browser-ready.
cardinality: Cardinality constraints over boolean ProofExpr atoms — the missing primitive that lets the certified solver answer “at most / at least / exactly k of these are true”. Encoded with Sinz’s sequential counter (linear in n·k, fresh auxiliary atoms under a caller-chosen prefix), so the result is an ordinary boolean obligation the existing CNF/CDCL/RUP pipeline discharges. This is the building block for SAT-based optimization (crate::optimize).
category_collapse: The category of collapses — the 2-rung toward the ∞-tower.
cdcl: A conflict-driven clause-learning (CDCL) SAT core — the modern competition-grade engine, built to the lineage that made SAT practical: two-watched-literal unit propagation (Moskewicz et al., Chaff, 2001), first-UIP conflict analysis with learned clauses and non-chronological backtracking (Marques-Silva & Sakallah, GRASP, 1996), VSIDS-style activity decisions, and Luby restarts (Luby et al., 1993). The clean reference implementation it follows is Eén & Sörensson’s MiniSat (2003).
census: The small-n SAT-space census — the measurement instrument.
certifier: The Certifier: Converts DerivationTrees to Kernel Terms.
cnf: Tseitin clausification: a grounded, quantifier-free ProofExpr → CNF over the CDCL core’s Lits (Tseitin, 1968 — the standard linear-size equisatisfiable transform that introduces one auxiliary variable per compound subformula). This is the bridge from the logic-grid encoding (closures, at-most-one, of-pair, clue clauses) to the crate::cdcl SAT engine, giving the Untrusted trust tier: solve premises ∧ ¬goal; UNSAT ⇒ the goal is entailed. The same CNF feeds the RUP checker (the fast trust tier) and is the input an AllDifferent GAC propagator filters.
coalgebra: The coalgebraic / Poly view, made into checked code rather than narration.
cofactor: The cofactor-DAG lens: symmetry above the instance.
complexity: Certified complexity bounds — a refutation that carries a checkable proof of its own size.
counterexample: Counterexamples — when a goal is FALSE, exhibit a model instead of failing silently. Lean ships no built-in counterexample finder with its automation; this closes that gap.
counting_principle: Fast refuter for the modular counting principle Count_q(n): partition an n-element set into blocks of size q. Encoded as: one Boolean per q-subset (block); a coverage clause per element (the incident blocks, at least one chosen); and a disjointness clause for every pair of overlapping blocks. It is unsatisfiable exactly when q ∤ n.
crush: crush — the grind-style closer: E-match quantified equality lemmas into the ground e-graph, then discharge the goal by certified congruence closure.
cubical: A general d-dimensional cubical-homology engine — one engine, every rung of the ladder.
cyclotomic: Power-of-two cyclotomic ring R = ℤ[X]/(Xⁿ + 1), n = 2ᵏ
decide: decide — proof by evaluation for closed decidable goals.
development: A formal-development parser: the body of a ## Theory block — a sequence of Axiom and Theorem declarations in formal notation — into the axioms and LibraryTheorems the multi-theorem driver consumes.
dimacs: DIMACS CNF parsing and printing — the SAT-competition interchange format, and the front door for running arbitrary instances through the solver.
discrimination: First-order discrimination tree: the shared pattern index under simp rule lookup, exact?/apply? library search, and crush’s E-matching.
eilenberg_maclane: The general Eilenberg–MacLane construction K(A, n) — one engine, every rung of the tower.
elliptic: Elliptic-curve primitives over ℤ/N — the additive→multiplicative lift
engine: Backward chaining proof engine.
error: Error types for proof search and unification.
factor: Structural factoring: the AIT thesis applied to public-key crypto.
families: Parametric generators for symmetry-rich SAT families — the canonical hard cases where symmetry breaking earns its keep. They are programmatic (reproducible, offline, parametric) rather than vendored .cnf files, and each is pinned to its known verdict so the solver and the certified pipeline can be tested against ground truth.
formula: A self-contained parser from formal first-order-logic surface text to ProofExpr.
fp2: 𝔽_{p²} arithmetic and the supersingular isogeny graph
gf2: The general linear group GL(n,2) and the invertibility constant — where the reciprocal SAT-threshold sum comes home.
grid_solver: A fast, certified finite-domain (logic-grid) solver.
grounding: Finite-domain grounding.
groupoid: The action groupoid — what symmetry breaking means, categorically, as checked code.
hints: Socratic Hint Engine - Generates pedagogical hints for proof guidance.
hornsat: Horn-SAT in linear time via unit propagation (forward chaining).
hypercube: The Boolean hypercube {0,1}ⁿ and its subcube cover — the geometric substrate beneath SAT, and the executable form of Pnp.lean’s HypercubeSAT (the Lean formalization lives at work/Pnp.lean).
hyperelliptic: Genus-2 curves and the Richelot (2,2)-isogeny — the abelian-surface mechanism
inprocess: Certified inprocessing: clause-database simplifications that emit a machine-checkable proof.
interval_sched: Interval scheduling in O(n log n) via a sweep line — the matching/Hall reasoner reaching into resource allocation over time.
isogeny: Certified isogeny torsion-image witnesses — the SIDH/SIKE public-data structure, in the prover
kan_complex: Actually having an ∞-groupoid — not its invariants, the object itself, with its defining property machine-verified.
lattice: LLL lattice reduction — the geometric lens of the compression campaign.
lemma_index: exact? / apply? and premise selection: search over a NAMED, certified lemma library.
linarith_solve: The decision core for linear integer arithmetic: Fourier-Motzkin elimination that tracks the non-negative combination it eliminates with, so an unsatisfiable system yields its Farkas certificate — the multipliers λᵢ ≥ 0 on the original constraints such that Σ λᵢ·constraintᵢ is a positive constant ≤ 0 (a contradiction). The proof engine reconstructs a kernel proof from those multipliers via le_mul_nonneg/le_add_mono + the Bool no-confusion discriminator. Pure and self-contained — no kernel, no certificates here.
lll: Satisfiability from sparsity — the Lovász Local Lemma certificate and its constructive Moser–Tardos witness. The lower bookend to the first-moment bound.
lyapunov: Lyapunov-function synthesis — don’t search for the proof, discover the measure that collapses the problem, and let the proof fall out as a corollary.
matching: Certified bipartite-matching infeasibility — the polynomial reasoner for pigeonhole-shaped problems that are exponential for resolution (and therefore for any CDCL SAT solver, ours included).
modm: Linear algebra over ℤ/m for composite m, by the Chinese Remainder Theorem — the multiplicative symmetry break. A system Σ aᵢ·xᵢ ≡ c (mod m) over a squarefree modulus m = p₁·…·p_t factors, through the ring isomorphism ℤ/m ≅ GF(p₁) × … × GF(p_t), into one independent system over each prime field — each decided by crate::modp::solve — and the per-field solutions are recombined by CRT. The factorization of the modulus is the symmetry that splits the problem; the prime fields are the irreducible pieces:
modp: Linear algebra over GF(p) — the mod-p generalization of the GF(2) parity cut (crate::xorsat).
omega_solve: omega — linear INTEGER arithmetic, the discreteness-aware layer over the rational Farkas core.
optimize: Certified SAT-based optimization. We have no native MaxSAT/ILP solver, so we minimise an integer cost the honest way: binary-search the smallest feasible cost bound, where each query is a certified decision (prove_unsat → Sat witness or RUP-Refuted). The result is a certified optimum — a witness at the optimum and a refutation at optimum−1 — not merely a value we happened to find.
orbit_stability: Orbit stability: deciding symmetric Nullstellensatz questions at every scale by one finite computation. The machinery behind the ∀m lower-bound program.
ordering: The ordering-principle specialist — a polynomial-time recognizer + refuter for GT(n), the linear-ordering contradiction. GT(n) asserts a strict total order (totality + antisymmetry + transitivity) in which every element has a strictly greater one (“no maximum”). That is impossible: a finite strict total order always has a maximum. So a complete GT(n) core is unsatisfiable, and any formula containing it (a superset of an UNSAT core) is UNSAT.
parity_cardinality: Fast refuter for the coupled exactly-one + parity family. An exactly-one group (an at-least-one clause plus the full at-most-one clique over its variables) forces EXACTLY one of its selectors true, so their XOR is 1 (odd). If the formula’s parity substructure forces that same XOR to 0 (even), the two are inconsistent and the formula is UNSAT — the mixed obstruction neither theory sees alone.
period: The period / order seam — the classical shell of Shor’s algorithm
permgroup: Schreier–Sims: a base and strong generating set (BSGS) for a permutation group — the non-abelian generalization of Gaussian elimination, and the last rung of the algebra ladder (GF(2)→GF(p)→ℤ/m linear; this is the group level).
pigeonhole: Pigeonhole / bipartite-matching detection for the general solver — the cardinality reasoning that lets prove_unsat win on pigeonhole-shaped formulas in POLYNOMIAL time.
polycalc: Polynomial Calculus / Nullstellensatz over GF(2) — the algebraic proof system that subsumes the linear cuts (parity is its degree-1 fragment) and, at higher degree, refutes strictly more.
polycalc_gfp: Nullstellensatz over any prime field GF(p) and over GF(4) — the characteristic axis of the algebraic proof system that crate::polycalc fixes at GF(2).
polycalc_zm: Nullstellensatz over the rings ℤ/m — composite moduli, zero divisors and all, at arbitrary degree. The characteristic axis (crate::polycalc_gfp) covered every field; this module covers what is left of “GF(N) for any N”: the moduli where no field exists (ℤ/6) and the prime powers where the ring is not the field (ℤ/4, with its nilpotent 2).
postnikov: The Postnikov k-invariant — the gluing data of a 2-type, and the obstruction to breaking it into a product.
pr: The PR (propagation-redundancy) checker — the trust tier for model-removing clause additions, and the keystone that makes certified symmetry breaking possible.
progress_complex: Genuine higher homotopy, at last — π₁ ≠ 0 from real concurrency, the hole is the deadlock.
proof: Shared proof-step vocabulary for the certified checkers.
proof_emit: Standard proof-trace emission — DRAT, LRAT, and DPR text from our in-memory ProofStep stream, so the certified refutations this crate produces are not merely self-checked but replayable by the SAT community’s independent (and in cake_lpr’s case formally verified) checkers.
proof_rewrite: The proof-rewrite 2-cells — independent refutation steps commute, and the commutation squares make the space of proof-orderings a contractible CAT(0) cube complex. This is the honest higher structure the symmetry tower pointed at, and it is genuine 2-dimensional homotopy: not a faked π₂, but the coherence theorem for proofs — every way of reordering independent steps is coherently the same, up to all higher homotopies.
pseudo_boolean: Pseudo-Boolean constraints + cutting planes — a proof system STRICTLY STRONGER than resolution.
register_alloc: Certified linear-scan register allocation — the matching/Hall reasoner as a compiler back-end.
res_width: Certified resolution-width lower bounds — the third proof system of the separations atlas, with the same zero-trust certificate discipline as the Nullstellensatz dual witnesses.
rule_search: aesop-style rule-set search: turn auto’s fixed cascade into an extensible, best-first search over registered rules.
rup: The RUP (Reverse Unit Propagation) linear checker — the fast default trust tier.
sat: Propositional SAT-discharge of a ProofExpr obligation — the engine behind in-browser, Z3-free hardware proving.
satcli: The SAT command-line driver shared by logos-sat and largo sat.
sdcl: Satisfaction-Driven Clause Learning (Heule, Kiesl & Seidl) — the engine that reasons at the Extended-Frege level by discovering propagation-redundant clauses, not just learning implied ones. It is symmetry breaking taken to its limit: where certified symmetry breaking needs an automorphism to supply a witness, SDCL finds the witness by solving the positive reduct — a smaller SAT problem — so it works on any structure, symmetric or not.
simp: simp rule sets: oriented rewrite rules compiled from proved lemmas, indexed for fast lookup, instantiated by matching.
solve: Structure-detecting solve front-end — the auto-dispatcher that puts our whole arsenal behind a single entry point.
sos: Sum-of-Squares / Positivstellensatz refutation over ℚ — kept EXACT (no SDP, no floating point) by the LP slice of the cone. True SoS is a semidefinite program over the reals; that would forfeit our certified guarantee. Instead we take the diagonal (fixed-square-basis) Positivstellensatz, which is an exact rational linear program: a CNF is lifted to degree-2 pseudo-Boolean inequalities and the lift is refuted by exact Fourier–Motzkin / Farkas elimination.
steenrod: The Steenrod algebra acting on H*(BZ/2; Z/2) = Z/2[x] — the deepest layer of cohomology operations, and a place where homotopy theory turns out to be number theory.
sym_break: Complete lex-leader symmetry breaking, driven by the Schreier–Sims backend.
sym_certify: Certified symmetry breaking — the centerpiece. Given a formula and a set of verified symmetry generators, add lex-leader symmetry-breaking predicates as PR steps (each self-checked, fail-closed), solve the augmented formula, and emit a single composed refutation that an independent checker accepts against the original formula alone.
sym_dynamic: Dynamic symmetry breaking — Symmetric Explanation Learning (SEL), the in-search tier.
symmetry: Symmetry breaking for the general solver — the second pillar (with crate::pigeonhole cardinality reasoning) for winning on pigeonhole.
symmetry_detect: General symmetry detection for CNF — the engine behind certified symmetry breaking.
tactic: A tactic framework with a first-class goal state — the interactive proof interface (ROOT R5 of the Lean-competitive architecture).
tactic_script: A tiny proof-script language over the crate::tactic combinators — proofs as TEXT, the way a Lean/Coq proof reads. This is the self-contained seam toward a full English vernacular: it has no dependency on the surface language, so it compiles a script string straight into a composed Tactic.
trace_determinism: The concurrency tie made literal: determinism = contractibility, on a real machine.
two_group: The 2-group frontier — climbing past K(G,1) to genuine 2-types, honestly.
two_type: A genuinely 2-truncated ∞-groupoid, had as an object: the minimal K(A, 2).
twosat: 2-SAT in linear time via the implication graph + strongly-connected components.
unify: First-order unification for proof search.
verify: Unified theorem verification — the single door.
xor_drat: The CNF→GF(2) bridge: compile a Gaussian (XOR linear-dependency) refutation into a strict DRAT proof that an external checker (drat-trim) accepts.
xor_engine: DPLL(XOR) — the live GF(2) reasoning engine.
xorsat: XOR-SAT via Gaussian elimination over GF(2) — the parity analog of the pigeonhole/matching supercrush.

Structs§

DerivationTree: The “Euclidean Structure” - A recursive tree representing the proof.
InductionArg: One argument of a constructor in an InductionCase.
InductionCase: The “Lever” - The specific logical move made at each proof step.
MatchArm: A single arm in a match expression. Example: Succ(k) => Add(k, m)
ProofGoal: The Goal State for the Backward Chainer.

Enums§

InferenceRule
ProofExpr: Owned expression representation for proof manipulation.
ProofTerm: Owned term representation for proof manipulation.