Synthesis of Recursive Programs in Saturation

EasyChair Preprint 12145

Abstract

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

@booklet{EasyChair:12145,
  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 12145},
  year      = {EasyChair, 2024}}