TIP: tons of inductive problems

DOI10.1007/978-3-319-20615-8_23zbMATH Open1417.68179OpenAlexW2109261022MaRDI QIDQ3453129FDOQ3453129

Dan Rosen, Nicholas Smallbone, Moa Johansson, Koen Claessen

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://research.chalmers.se/en/publication/222739

Recommendations

• TIP: tools for inductive provers
• Inductive benchmarks for automated reasoning
• The TPTP problem library
• Strategic issues, problems and challenges in inductive theorem proving
• TPTP, TSTP, CASC, etc.

Mathematics Subject Classification ID

Cites Work

• Automating Induction with an SMT Solver
• Zeno: An Automated Prover for Properties of Recursive Data Structures
• Induction for SMT Solvers
• Hipster: Integrating Theory Exploration in a Proof Assistant
• Automating Inductive Proofs Using Theory Exploration
• Productive use of failure in inductive proof
• TIP: Tons of Inductive Problems
• Case-Analysis for Rippling and Inductive Proof

Cited In (9)

• Quantifier-free induction for lists
• Inductive benchmarks for automated reasoning
• TIP: Tons of Inductive Problems
• Conjectures, tests and proofs: an overview of theory exploration
• Theory exploration powered by deductive synthesis
• Unprovability results for clause set cycles
• Integer induction in saturation
• Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
• Induction and Skolemization in saturation theorem proving

Uses Software

• Dafny
• SMT-LIB
• Zeno
• HipSpec
• CVC4
• Hipster
• Pirate
• GitHub

This page was built for publication: TIP: tons of inductive problems

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