Automatic Deductive Synthesis of Lisp Programs in the System ALISA

Abstract

The work deals with deductive synthesis of functional programs. During this synthesis formal specification of a program is taken as a mathe-matical existence theorem and while proving it, we derive a program and prove that this program corresponds to given specification. Our method of synthesis is based on the deductive tableau method, that allows to derive three basic constructions of a functional program. But the full search of possible proof attempts in the deductive tableau induces a very large search space; the proof is needed to be guided. For using this method in the automatic mode additional heuristics are required. Some of such heuristics are proposed in this work. They consist in proof planning by using rippling and in the use of sorted logic with type hierarchy that reduces search space and blocks some branches of proof, corresponding to synthesis of incorrect functions. The proposed techniques are implemented in the system ALISA and used for automatic synthesis of several functions on Lisp language.