Program Synthesis in Saturation

EasyChair Preprint 10223

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.

Keyphrases: program synthesis, saturation, superposition, theorem proving

@booklet{EasyChair:10223,
  author    = {Petra Hozzová and Laura Kovács and Chase Norman and Andrei Voronkov},
  title     = {Program Synthesis in Saturation},
  howpublished = {EasyChair Preprint 10223},
  year      = {EasyChair, 2023}}