Induction in saturation-based proof search

DOI10.1007/978-3-030-29436-6_28OpenAlexW2921114217MaRDI QIDQ2305434

Andrei Voronkov, Giles Reger

Publication date: 10 March 2020

Full work available at URL: https://www.research.manchester.ac.uk/portal/en/publications/induction-in-saturationbased-proof-search(7d7db466-3d15-4ac6-9b21-38400bb95257).html

Mathematics Subject Classification ID

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

Related Items (6)

Inductive benchmarks for automated reasoning ⋮ Getting saturated with induction ⋮ Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments ⋮ Integer induction in saturation ⋮ Unprovability results for clause set cycles ⋮ Induction and Skolemization in saturation theorem proving

Uses Software

• VAMPIRE
• SMT-LIB
• TPTP
• Zeno
• StarExec
• E Theorem Prover
• AVATAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Superposition with structural induction
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Combining Superposition and Induction: A Practical Realization
• Automating Induction with an SMT Solver
• Zeno: An Automated Prover for Properties of Recursive Data Structures
• AVATAR: The Architecture for First-Order Theorem Provers
• A decision procedure for term algebras with queues
• Extensional Crisis and Proving Identity
• Automating Inductive Proofs Using Theory Exploration
• Induction for SMT Solvers
• Coming to terms with quantified reasoning
• Theorem Proving in Higher Order Logics

This page was built for publication: Induction in saturation-based proof search