Attributed To Prove The Tree Extraction Procedure

For theorem proving problem such like (Vx)(3y)P(x,y), we can answer whether it is true or not by using the resolution principle. But, for the classical proof theory as "for every certain x, how to find value of y?", the resolution principle is unavailable. Many people research how to find value of y from resolution proof trees. The exemplary method was shown by Green and Luckham. But there are many limitations in their methods because the methods are not based on analysis of resolution proof procedure.In this paper, we do two things. First, for theorem proving problem such like (Vx)(3y)P(x,y), we present a method for extracting procedure from the proofs generated by the resolution principle. It extracts process information from the proof tree by analyzing every node of resolution proof tree to extract procedure. And the partial correctness of the extracted procedure is proved. Second, for theorem proving problem such like (Vx)(3y)(\/z)P(x,y,z) , resolution proof tree must include Skolem functions, the extracted procedure from this kind of resolution proof tree may include Skolem functions. 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 shown.The feature of this method is that the time and place complexities of the extracting method are both linear, and the extracting method itself is very simple, and can be implemented easily.