Download PDFOpen PDF in browser

Towards Synthesis in Superposition

EasyChair Preprint 8182

4 pagesDate: June 4, 2022

Abstract

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:
@booklet{EasyChair:8182,
  author    = {Petra Hozzová and Laura Kovács and Andrei Voronkov},
  title     = {Towards Synthesis in Superposition},
  howpublished = {EasyChair Preprint 8182},
  year      = {EasyChair, 2022}}
Download PDFOpen PDF in browser