Towards Synthesis in Superposition

EasyChair Preprint no. 8182

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

@Booklet{EasyChair:8182,
  author = {Petra Hozzová and Laura Kovács and Andrei Voronkov},
  title = {Towards Synthesis in Superposition},
  howpublished = {EasyChair Preprint no. 8182},

  year = {EasyChair, 2022}}