# Theory Exploration Powered By Deductive Synthesis

arXiv: https://arxiv.org/abs/2009.04826 · HTML: https://mlsanity.com/paper/2009.04826/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Sep 2020.

## Built on by (most cited first, 3 of 3)

- [Anti-unification and Generalization: A Survey](https://mlsanity.com/paper/2302.00277/) (2023)
- [A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam](https://mlsanity.com/paper/2504.04945/) (2025)
- [Can LLM Aid in Solving Constraints with Inductive Definitions?](https://mlsanity.com/paper/2603.03668/) (2026)

## Abstract (arXiv)

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.