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

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