TIP: tons of inductive problems

DOI10.1007/978-3-319-20615-8_23MaRDI QIDQ3453129zbMATH OpenOpenAlexFDO

Authors Koen Claessen, Moa Johansson, Dan Rosen, Nicholas Smallbone

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

Mathematics Subject Classification ID

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.

Cites work

• Automating Induction with an SMT Solver
• Automating Inductive Proofs Using Theory Exploration
• Case-analysis for rippling and inductive proof
• Hipster: integrating theory exploration in a proof assistant
• Induction for SMT solvers
• Productive use of failure in inductive proof
• TIP: tons of inductive problems
• Zeno: an automated prover for properties of recursive data structures

Cited in

(11)

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

Describes a project that uses

Uses Software

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

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)