Program Synthesis Based On General Resolution

Automatic programming is a very active area of research in computer science. It plays an important role in field of planning and robots in the realm of artificial intelligence. In the theory of programming, program synthesis is deeply concerned with program verification. Program synthesis extracts program from the automated theorem proving. That means, in order to construct a program satisfying certain specifications (usually represented in the form of a sequence of logical formulas), a theorem induced by those specifications is proved, and the desired program is extracted from the proof.For theorem proving problem such as ((?)x)((?)y)p(x, y), the general resolution principle can answer whether it is true or not, while for the classical proof theory as "for every certain x, how to find value of y?", the general resolution principle cannot give the answer by itself. A lot of recent research has concentrated on how to find value of y from the proof tress. While, because the methods are not based on the analysis of proof procedure, there are many limitations in their methods. For example, the former methods just can answer the sequential problem, or just can list all the possible answers while cannot find the answer under certain conditions.In this paper, two problems are solved. First, for theorem proving problem such as((?)x)((?)y)p(x, y), we present a method of extracting program from the proof generated by thegeneral resolution principle. It collects process information from the general resolution proof tree by analyzing every node of general resolution proof tree to extract program. And also, the partial correctness of the extracted program is proved. Second, for theorem proving problem such as((?)x)((?)y)((?)z)P(x,y,z), general resolution proof tree must include Skolem functions, so the extracted program from this kind of proof tree maybe include Skolem functions also. In this paper, a sufficient and necessary condition is given to judge whether Skolem functions can be eliminated from the extracted procedure or not, and the extracting method is put forward.The algorithm in this paper is applied to extract the sequential and branch program. In addition, the method can extract the recursive program when the theorems used in proving are in the recursive forms, and also can extract iterative program by mathematical induction.