Resolution Graphs

reportActive / Technical Report | Accession Number: ADA638143 | Open PDF

Abstract:

This paper introduces a new notation, called resolution graphs, 11 for deductions by resolution in first-order predicate calculus. A resolution graph consists of groups of nodes that represent initial clauses of a deduction and links that represent unifying substitutions. Each such graph uniquely represents a resultant clause that can be deduced by certain alternative but equivalent sequences of resolution and factoring operations. Resolution graphs are used to illustrate the significance of merges and tautologies in proofs by resolution. Finally, they provide a basis for proving the completeness of a proof strategy that combines the set of support, resolution with merging, linear format, and Lovelands subsumption conditions.

Author(s):
Yates, Robert A. ; Hart, Timothy P. ; Raphael, Bertram
Author Organization(s):
SRI INTERNATIONAL MENLO PARK CA
Descriptive Note:
Technical note no. 24
Pagination:
0062

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution:
Approved For Public Release
Distribution Statement:
Approved For Public Release; Distribution Is Unlimited.

RECORD

Collection: TR
Identifying Numbers
Contract/Grant Number(s):
F30602-69-C-0056, NAS12-2221
Monitor Series:
ARPA
 Subject Terms
Joint Capability Areas:
JCA_5_Command and Control; JCA_5.3_Planning; JCA_1_Force Support; JCA_1.2_Force Preparation; JCA_1.2.6_Concepts; JCA_5.2.2_Develop Knowledge and Situational Awareness; JCA_5.2_Understand; JCA_1.2.3_Educating; JCA_8_Building Partnerships
Modernization Areas:
Fully Networked C3
Communities of Interest:
C4I
Descriptor(s):
*CALCULUS, FORMATS, GRAPHS, RESOLUTION, SEQUENCES, STRATEGY
Field(s)/Group(s):
Numerical Mathematics
Keyword(s):
RESOLUTION GRAPHS
Report Date:
1970 Mar 01
Creation Date:
2016 Oct 03