Theory Exploration Powered By Deductive Synthesis

TL;DR

This paper introduces a purely deductive symbolic technique for bottom-up lemma discovery in theory exploration, eliminating the need for random testing and SMT solvers, and improving lemma generation efficiency.

Contribution

It presents a novel deductive approach for theory exploration that enhances lemma discovery without relying on random testing or SMT solvers.

Findings

Finds more lemmas than previous methods.

Avoids redundancy in lemma generation.

Enables reasoning with user-defined higher-order functions.

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.