Issue No.08 - August (1976 vol.25)
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.
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, August 1976, doi:10.1109/TC.1976.1674701