Towards Synthesis in Superposition

EasyChair Preprint 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 8182},
  year      = {EasyChair, 2022}}