# Program Synthesis in Saturation

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Feb 2024.

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

- [An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction](https://mlsanity.com/paper/2511.04092/) (2025)

## Abstract (arXiv)

We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis. This is an extended version of an Automated Deduction -- CADE 29 paper with the same title and the same authors.