Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Program Synthesis in Saturation

Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov

TL;DR

This work presents a method to synthesize recursion-free programs from functional specifications by running a saturation-based first-order theorem prover and extracting program fragments as witnesses. Central to the approach is the integration of answer literals into the saturation process, which records conditional program branches and enables the construction of final programs once branch conditions collectively cover all cases. The authors extend the superposition calculus with computable unifiers and provide a computable-unifier unification procedure, all implemented in Vampire and integrated with AVATAR, with experiments including cases not encodable by SyGuS. The results demonstrate that first-order proving can serve as an effective basis for deductive program synthesis, potentially enabling future extensions toward recursive programs and induction.

Abstract

We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis. This is an extended version of an Automated Deduction -- CADE 29 paper with the same title and the same authors.

Program Synthesis in Saturation

TL;DR

This work presents a method to synthesize recursion-free programs from functional specifications by running a saturation-based first-order theorem prover and extracting program fragments as witnesses. Central to the approach is the integration of answer literals into the saturation process, which records conditional program branches and enables the construction of final programs once branch conditions collectively cover all cases. The authors extend the superposition calculus with computable unifiers and provide a computable-unifier unification procedure, all implemented in Vampire and integrated with AVATAR, with experiments including cases not encodable by SyGuS. The results demonstrate that first-order proving can serve as an effective basis for deductive program synthesis, potentially enabling future extensions toward recursive programs and induction.

Abstract

We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis. This is an extended version of an Automated Deduction -- CADE 29 paper with the same title and the same authors.
Paper Structure (9 sections, 13 equations, 2 figures)

This paper contains 9 sections, 13 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Our approach in a nutshell.
  3. Contributions.
  4. Preliminaries
  5. Computable Symbols and Programs
  6. Saturation and Superposition
  7. Answer Literals
  8. Answer literals with $\mathtt{if}\!-\!\mathtt{then}\!-\!\mathtt{else}$.
  9. Illustrative Example

Figures (2)

  • Figure 1: The superposition calculus $\mathbb{S}\text{up}$.
  • Figure 2: Axioms defining a group. Uninterpreted function symbols $i(\cdot), e, *$ represent the inverse, the identity element, and the group operation, respectively.