Design And Implementation Of Program Synthesis Based On Resolution Principle

In general, design of program can be treated as theorem proving, so program synthesis has close relations with automatic theorem proving. Generally, only constructive proving can extract program. Though resolution principle is a reduction to absurdity, it has been known that linear program can be extracted from resolution principle, and it is already proved that branch program can be extracted from resolution principle. Essentially, not all of the proving of resolution principle is constructive, so not all loop program can be extracted from the proving. But loop program can be extracted from the proving of resolution principle with the aid of mathematical induction. In this paper, resolution principle is used to automatic theorem proving, then program is extracted from the proof tree constructed during proving.In this paper, we do three things. First, theorem-proving system is designed and implemented with C/C++ programming language on computer. This system can handle with the theorem and conclusion of the predication logic and judge whether the predication logic is true or not. A resolution strategy used in the system gets good results and makes full preparations for program extracting. Secondly, we design and implement the program to extract program from the proving process. This program can adequately analyze and deal with the information of the program proving process which is based on resolution principle. Also, it can rebuild the proof tree and generate programs from it in the way of program extracting. Thirdly, a new method is described for extracting circular programs with mathematical induction. And it can extract loop programs from the recursively described problems.The accomplishment of the method discussed in this article is restricted by computer resources, so it isn't universal. We bring forward some problems with regard to automated theorem proving based on resolution principle and program extracting. The settlement of these problems will make program synthesis and automated theorem proving applied.