Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

Publication in EndNote Format

%0 Report %@ 32 %A Luckham, David; Nilsson, Nils J. %T Extracting Information From Resolution Proof Trees %C 333 Ravenswood Ave, Menlo Park, CA 94025 %I AI Center, SRI International %D 1971 %K Proof Trees %X 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. %O TN 32 revised. SRI Project 8259. To appear in the AI Journal. Supported by ARPA order SD-183, and NASA contract NAS12-2221. %U http://www.ai.sri.com/pubs/files/1939.pdf

SRI International
©2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy