Inductive benchmarks for automated reasoning

DOI10.1007/978-3-030-81097-9_9MaRDI QIDQ2128807zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• TIP: tons of inductive problems
• Induction for SMT solvers
• Automating Induction with an SMT Solver
• Heaps and Data Structures: A Challenge for Automated Provers
• scientific article; zbMATH DE number 2177631

Cites work

• Dafny: an automatic program verifier for functional correctness
• eThor
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• Induction for SMT solvers
• Induction in saturation-based proof search
• Integer induction in saturation
• Superposition with structural induction
• The Imandra Automated Reasoning System (System Description)
• TIP: tons of inductive problems
• Zeno: an automated prover for properties of recursive data structures

Cited in

(7)

• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• GRUNGE: a grand unified ATP challenge
• TIP: tons of inductive problems
• TIP: tools for inductive provers
• Induction for SMT solvers
• Getting saturated with induction
• A mathematical benchmark for inductive theorem provers

Describes a project that uses

Uses Software

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

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

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