Inductive benchmarks for automated reasoning

DOI10.1007/978-3-030-81097-9_9zbMath1485.68281OpenAlexW3160880798MaRDI QIDQ2128807

Laura Kovács, Andrei Voronkov, Márton Hajdu, Johannes Schoisswohl, Petra Hozzová

Publication date: 22 April 2022

Full work available at URL: http://hdl.handle.net/20.500.12708/18558

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Getting saturated with induction

Uses Software

• Dafny
• VAMPIRE
• SMT-LIB
• NQTHM
• Zeno
• CVC4
• CBMC
• Easychair
• Imandra
• eThor

Cites Work

• Unnamed Item
• Superposition with structural induction
• Integer induction in saturation
• Induction with generalization in superposition reasoning
• Induction in saturation-based proof search
• Zeno: An Automated Prover for Properties of Recursive Data Structures
• Dafny: An Automatic Program Verifier for Functional Correctness
• TIP: Tons of Inductive Problems
• The Imandra Automated Reasoning System (System Description)
• Induction for SMT Solvers
• eThor

This page was built for publication: Inductive benchmarks for automated reasoning