Crate logicaffeine_proof 

Logicaffeine Proof Engine

Core structures for proof representation and verification.

This module defines the “Shape of Truth.” A proof is not a boolean; it is a recursive tree of inference rules that can be inspected, transformed, and verified.

Curry-Howard Correspondence

The proof engine implements the propositions-as-types paradigm:

• A Proposition is a Type — logical formulas correspond to types
• A Proof is a Program — derivation trees are proof terms
• Verification is Type Checking — the kernel validates proof terms

Architecture Invariant

This crate has no dependency on the language crate (Liskov boundary). The conversion from LogicExpr → ProofExpr lives in the language crate, ensuring the proof engine remains pure and reusable.

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

certifier

The Certifier: Converts DerivationTrees to Kernel Terms.

engine

Backward chaining proof engine.

error

Error types for proof search and unification.

hints

Socratic Hint Engine - Generates pedagogical hints for proof guidance.

unify

First-order unification for proof search.

Structs

DerivationTree

The “Euclidean Structure” - A recursive tree representing the proof.

MatchArm

A single arm in a match expression. Example: Succ(k) => Add(k, m)

ProofGoal

The Goal State for the Backward Chainer.

Enums

InferenceRule

The “Lever” - The specific logical move made at each proof step.

ProofExpr

Owned expression representation for proof manipulation.

ProofTerm

Owned term representation for proof manipulation.