Extracting information from resolution proof trees

摘要

Procedures for generating proofs within a logical inference system can be applied to many information-retrieval and automatic problem-solving tasks. These applications require additional procedures for extracting information from the proofs when they are found. We present an extraction procedure for proofs generated by the resolution principle. The procedure uses a given proof to find solutions for existential quantifiers in the statement proved in terms of known quantities in the initial data. This procedure relies heavily on basic subfunctions in the resolution program, so that it requires relatively little additional programming. The correctness of the procedure is proved, and examples are given to illustrate how it operates and to show that it cannot be simplified at certain points without loss of generality.