Download PDFOpen PDF in browser

Towards Synthesis in Superposition

EasyChair Preprint no. 8182

4 pagesDate: June 4, 2022


We present our ongoing developments in synthesizing recursion-free programs using the superposition reasoning framework in first-order theorem proving. Given a first-order formula as a program specification, we use a superposition-based theorem prover to establish the validity of this formula and, along this process, synthesize a function that meets the specification. To this end, we modify the rules of the superposition calculus to synthesize program fragments corresponding to individual clauses derived during the proof search. If a proof is found, we extract a program based on the found (correctness) proof. We implemented our approach in the first-order theorem prover Vampire and successfully evaluated it on a few example.

Keyphrases: automated deduction, program synthesis, superposition reasoning

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Petra Hozzová and Laura Kovács and Andrei Voronkov},
  title = {Towards Synthesis in Superposition},
  howpublished = {EasyChair Preprint no. 8182},

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