A nonclausal inference method for program derivation
Joseph Varghese · 1986
The goal of automatic programming research is the development of tools and methodologies that automate various phases of the programming process. Program synthesis is a technique for the automatic derivation of programs from their specifications. In this thesis, a method for deriving programs from abstract formal specifications is presented. The specifications are in first-order logical form and the target language is Horn clause logic. Since the formalisms are closely related, theorem proving techniques can be used to transform specifications to programs. The inference method is based on nonclausal resolution and uses the concepts of polarity and unification. Several program derivations are also presented for the purposes of illustration.