Program Synthesis in Saturation
Abstract
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.
Cite
@article{arxiv.2402.18962,
title = {Program Synthesis in Saturation},
author = {Petra Hozzová and Laura Kovács and Chase Norman and Andrei Voronkov},
journal= {arXiv preprint arXiv:2402.18962},
year = {2024}
}
Comments
23 pages; this is an extended version of the published paper