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 Details

Extracting Information From Resolution Proof Trees

by Luckham, David; Nilsson, Nils J.

Technical Note 32
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave, Menlo Park, CA 94025
Jan 1971.

Note: TN 32 revised. SRI Project 8259. To appear in the AI Journal. Supported by ARPA order SD-183, and NASA contract NAS12-2221.

Order an AIC Technical Note

Abstract

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.

Electronic Copies


Adobe PDF

BibTeX

EndNote

AIC Personnel

Name Title E-mail
Nilsson, Nils J Alumnus

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