ИСТИНА

The work concerns deductive synthesis of functional programs from logic-based specifications. During this synthesis formal specification of a program is taken as a mathematical existence theorem and while proving it, we derive a program and simultaneously 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. We propose to plan the proof using rippling and also to use 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.