AUTOMATIC PROGRAM SYNTHESIS USING KNOWLEDGE BASE AND THEOREM PROVING TECHNIQUES

Abstract

This dissertation addresses the problem of develop-ing an automatic program synthesizer. The problem has been tackled using knowledge base and theorem proving techniques. A framework for a rule based automatic program synthesizer for the problems of set theory has been developed. The required knowledge base consisting of knowledge about problem domain and target language has been created. The control mechanism of pattern directed function invocation has been used to invoke the appropriate rules in the process of synthesizing the programs in a LISP-like language. The technique of theorem proving has been applied to synthesize the programs for simple computational problems. Resolution mechanism has been used as theorem prover in the automatic synthesis of programs for trivial programming problems. The validity of both the techniques has been esta-bushed by actually generating sample programs. It has been observed that knowledge base approach is bit lengthy and cumbersome as it requires a large amount of knowledge about the whole synthesizing process but it is quite effi.-cient as it makes use of heuristics. In the theorem proving approach a constructed program comes with a proof of its correctness.