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

Full work available at URL https://doi.org/10.4204/EPTCS.337.4

Mathematics Subject Classification ID

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

Cites work

• A combinator-based superposition calculus for higher-order logic
• A Polymorphic Vampire
• Automating induction by reflection
• Automating Induction with an SMT Solver
• AVATAR: The Architecture for First-Order Theorem Provers
• 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
• scientific article; zbMATH DE number 5959536 (Why is no real title available?)
• scientific article; zbMATH DE number 1324440 (Why is no real title available?)
• 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)