Automating Inductive Proofs Using Theory Exploration
From MaRDI portal
Publication:4928454
DOI10.1007/978-3-642-38574-2_27zbMath1381.68263OpenAlexW123460044MaRDI QIDQ4928454
Moa Johansson, Dan Rosen, Koen Claessen, Nicholas Smallbone
Publication date: 14 June 2013
Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)
Full work available at URL: https://research.chalmers.se/en/publication/175485
Related Items (23)
Theory exploration powered by deductive synthesis ⋮ Proving properties of functional programs by equality saturation ⋮ TIP: Tons of Inductive Problems ⋮ Inductive Prover Based on Equality Saturation for a Lazy Functional Language ⋮ Disproving Inductive Entailments in Separation Logic via Base Pair Approximation ⋮ Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Equivalence checking of two functional programs using inductive theorem provers ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ Alien coding ⋮ Into the Infinite - Theory Exploration for Coinduction ⋮ Machine Learning for Inductive Theorem Proving ⋮ Getting saturated with induction ⋮ Lemmaless induction in trace logic ⋮ Quick specifications for the busy programmer ⋮ Combining induction and saturation-based theorem proving ⋮ Integer induction in saturation ⋮ Induction in saturation-based proof search ⋮ Unnamed Item ⋮ Hipster: Integrating Theory Exploration in a Proof Assistant ⋮ Unprovability results for clause set cycles ⋮ Induction and Skolemization in saturation theorem proving ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ Inductive theorem proving based on tree grammars
Uses Software
This page was built for publication: Automating Inductive Proofs Using Theory Exploration
