This Article 
 Bibliographic References 
 Add to: 
August 1976 (vol. 25 no. 8)
pp. 823-835
S. Sickel, Department of Information Sciences, University of California
This paper presents a new representation and technique for proving theorems automatically that is both computationally more effective than resolution and permits a clear and concise formal description. A problem in automatic theorem proving can be specified by a set of clauses, containing literals, that represents a set of axioms and the negation of a theorem to be proved. The set of clauses can be replaced by a graph in which the nodes represent literals and the edges link unifiable complements. The nodes are partitioned by clause membership, and the edges are labeled with a most general unifying substitution. Given this representation, theorem proving becomes a graph-searching problem. The search technique presented here, in effect, unrolls the graph into sets of solution trees. The trees grow in a well-defined breadth-first way that defines a measure of proof complexity.
Index Terms:
Clause graphs, consistency of substitutions, resolution, unifers.
S. Sickel, "A Search Technique for Clause Interconnectivity Graphs," IEEE Transactions on Computers, vol. 25, no. 8, pp. 823-835, Aug. 1976, doi:10.1109/TC.1976.1674701
Usage of this product signifies your acceptance of the Terms of Use.