Download PDFOpen PDF in browser

Synthesis of Recursive Programs in Saturation

EasyChair Preprint no. 12145

48 pagesDate: February 16, 2024


We turn saturation-based theorem proving into an automated framework for recursive program synthesis. We introduce magic axioms as valid induction axioms and use them together with answer literals in saturation. We introduce new inferences rules for induction in saturation and use answer literals to synthesize recursive functions from these proof steps. Our proof-of-concept implementation in the Vampire theorem prover constructs recursive functions over algebraic data types, while proving inductive properties over these types.

Keyphrases: induction, program synthesis, recursion, saturation, superposition, theorem proving

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Petra Hozzová and Daneshvar Amrollahi and Márton Hajdu and Laura Kovács and Andrei Voronkov and Eva Maria Wagner},
  title = {Synthesis of Recursive Programs in Saturation},
  howpublished = {EasyChair Preprint no. 12145},

  year = {EasyChair, 2024}}
Download PDFOpen PDF in browser