Module proof_convert 

Conversion from parser AST to proof engine representation.

This module bridges the parser’s arena-allocated AST (LogicExpr<'a>) to the proof engine’s owned representation (ProofExpr).

The conversion clones all data into owned Strings, enabling proof trees to persist beyond the arena’s lifetime. Symbols are resolved using the interner at conversion time.

Key Function

logic_expr_to_proof_expr is the main entry point for converting parsed expressions to the format expected by the proof search engine.

Structs

DefaultRule

Convert a Term to ProofTerm. A defeasible default extracted by logic_expr_to_proof_expr_defeasible: the abnormality predicate guarding one GEN rule or implicature.

Functions

instantiate_var_with_constant

Substitute a free variable from with the CONSTANT to inside a ProofExpr — the operation that turns a wh-question body φ(x) into a candidate goal φ(c), so “who/what is …?” is answered by enumerating domain individuals and proving each candidate. Stops at a quantifier that re-binds from (capture avoidance).

logic_expr_to_proof_expr

Convert a LogicExpr to ProofExpr.

logic_expr_to_proof_expr_defeasible

Convert with DEFEASIBLE semantics: a generic GEN x(R(x) → N(x)) becomes the abnormality-guarded ∀x((R(x) ∧ ¬ab_k(x)) → N(x)), and an implicature is asserted under its own guard (assertion ∧ (¬ab_k → implicature)). The circumscription itself — minimizing each ab_k — happens in the defeasible reasoner; this conversion only preserves what the strict export (Generic → ∀, implicature dropped) erases.

term_to_proof_term