Theory exploration powered by deductive synthesis
From MaRDI portal
Publication:832255
DOI10.1007/978-3-030-81688-9_6zbMATH Open1493.68388arXiv2009.04826OpenAlexW3185574054MaRDI QIDQ832255FDOQ832255
Authors: Eytan Singher, Shachar Itzhaky 
Publication date: 25 March 2022
Abstract: Recent years have seen tremendous growth in the amount of verified software. Proofs for complex properties can now be achieved using higher-order theories and calculi. Complex properties lead to an ever-growing number of definitions and associated lemmas, which constitute an integral part of proof construction. Following this -- whether automatic or semi-automatic -- methods for computer-aided lemma discovery have emerged. In this work, we introduce a new symbolic technique for bottom-up lemma discovery, that is, the generation of a library of lemmas from a base set of inductive data types and recursive definitions. This is known as the theory exploration problem, and so far, solutions have been proposed based either on counter-example generation or the more prevalent random testing combined with first-order solvers. Our new approach, being purely deductive, eliminates the need for random testing as a filtering phase and for SMT solvers. Therefore it is amenable compositional reasoning and for the treatment of user-defined higher-order functions. Our implementation has shown to find more lemmas than prior art, while avoiding redundancy.
Full work available at URL: https://arxiv.org/abs/2009.04826
Recommendations
- scientific article; zbMATH DE number 1552527
- Conjecture synthesis for inductive theories
- Theory by process
- Exploring theories with a model-finding assistant
- scientific article; zbMATH DE number 1746693
- Deductive models and practical reasoning
- A new methodology for developing deduction methods
- Deciding Combinations of Theories
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Dafny: an automatic program verifier for functional correctness
- Simplify: a theorem prover for program checking
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Induction for SMT solvers
- Hipster: integrating theory exploration in a proof assistant
- Fast Decision Procedures Based on Congruence Closure
- Automating Inductive Proofs Using Theory Exploration
- Equality saturation
- Synthesis of circular compositional program proofs via abduction
- Conjecture synthesis for inductive theories
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Programming by demonstration using version space algebra
- Title not available (Why is that?)
- Superposition with structural induction
- Synthesis with abstract examples
- Program synthesis with equivalence reduction
- Maximal specification synthesis
- Congruence Closure with Free Variables
- TIP: tons of inductive problems
- Title not available (Why is that?)
- Quick specifications for the busy programmer
- Case-analysis for rippling and inductive proof
- Into the Infinite - Theory Exploration for Coinduction
- Fast congruence closure and extensions
Cited In (1)
Uses Software
This page was built for publication: Theory exploration powered by deductive synthesis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832255)
