Theory exploration powered by deductive synthesis

DOI10.1007/978-3-030-81688-9_6MaRDI QIDQ832255zbMATH OpenOpenAlexFDO

Authors Eytan Singher, Shachar Itzhaky

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2009.04826

zbMATH Keywords

synthesisautomatic theorem provingtheory exploration

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

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

Cites work

• scientific article; zbMATH DE number 1822263 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
• Automating Inductive Proofs Using Theory Exploration
• Case-analysis for rippling and inductive proof
• Congruence closure with free variables
• Conjecture synthesis for inductive theories
• Dafny: an automatic program verifier for functional correctness
• Equality saturation
• Fast Decision Procedures Based on Congruence Closure
• Fast congruence closure and extensions
• Hipster: integrating theory exploration in a proof assistant
• Induction for SMT solvers
• Into the Infinite - Theory Exploration for Coinduction
• Maximal specification synthesis
• Program synthesis with equivalence reduction
• Programming by demonstration using version space algebra
• Quick specifications for the busy programmer
• Simplify: a theorem prover for program checking
• Superposition with structural induction
• Synthesis of circular compositional program proofs via abduction
• Synthesis with abstract examples
• TIP: tons of inductive problems
• \textit{Theorema}: Towards computer-aided mathematical theory exploration

Cited in

(1)

• A synthesis of Hempelian and hypothetico-deductive confirmation

Describes a project that uses

Uses Software

• Coq
• Dafny
• Theorema
• VAMPIRE
• z3
• SIMPLIFY
• HipSpec
• Leon
• CVC4
• Hipster
• TRANSIT
• FlashMeta
• egg
• IsaCoSy

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)