Automated Synthesis of Recursive Programs from a ∀∃ Logical Specification.

The specification of a function is often given by a logical formula, called a ∀∃-formula, of the following form: ∀x∃yΦ(x,y). More precisely, a specification is given in the context of a certain theory E and is stated by the judgment E ⊢ ∀x∃y Φ(x,y). In this paper, we consider the case in which E is an equational theory. It is divided into two parts. In the first part, we develop a theory for the automated proof of such judgments in the initial model of E . The validity in the initial model means that we consider not only equational theorems but also inductive ones. From our theory we deduce an automated method for the proof of a class of such judgments. In the second part, we present an automatedmethod for program synthesis. We show how the previous proof method can be used to generate a recursive program for a function f that satisfies a judgment E ⊢ ∀x Φ(x, f(x)). We illustrate our method with the automated synthesis of some recursive programs on domains such as integers and lists. Finally, we describe our system LEMMA, which is an implementation in Common Lisp of these new methods. [ABSTRACT FROM AUTHOR]