The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.08 - August (1976 vol.25)
pp: 823-835
S. Sickel , Department of Information Sciences, University of California
ABSTRACT
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.
CITATION
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
29 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool