Automating induction by reflection

DOI10.4204/EPTCS.337.4MaRDI QIDQ6940479zbMATH OpenFDO

Authors Johannes Schoisswohl, Laura Kovács

Publication date 19 August 2025

Copyright license Creative Commons license

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 5959536 (Why is no real title available?)
• scientific article; zbMATH DE number 1324440 (Why is no real title available?)
• A Polymorphic Vampire
• A combinator-based superposition calculus for higher-order logic
• AVATAR: The Architecture for First-Order Theorem Provers
• Automating Induction with an SMT Solver
• Automating induction by reflection
• Combining induction and saturation-based theorem proving
• Combining superposition and induction: a practical realization
• Coming to terms with quantified reasoning
• Equivalence properties by typing in cryptographic branching protocols
• Induction for SMT solvers
• Induction in saturation-based proof search
• Induction with generalization in superposition reasoning
• Inferring inductive invariants from phase structures
• Mechanizing structural induction. II: Strategies
• Milestones from the Pure Lisp Theorem Prover to ACL2
• Superposition for -free higher-order logic
• Superposition with structural induction
• The new rewriting engine of dedukti (system description)
• Unification with abstraction and theory instantiation in saturation-based reasoning

Cited in

(1)

• Automating induction by reflection

This page was built for publication: Automating induction by reflection

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6940479)