×

Clause trees: A tool for understanding and implementing resolution in automated reasoning. (English) Zbl 1017.03506

Summary: A new methodology/data structure, the clause tree, is developed for automated reasoning based on resolution in first order logic. A clause tree \(T\) on a set \(S\) of clauses is a 4-tuple \({\langle}N, E, L, M{\rangle}\), where \(N\) is a set of nodes, divided into clause nodes and atom nodes, \(E\) is a set of edges, each of which joins a clause node to an atom node, \(L\) is a labeling of \(N{\cup}E\) which assigns to each clause node a clause of \(S\), to each atom node an instance of an atom of some clause of \(S\), and to each edge either \(+\) or \(-\). The edge joining a clause node to an atom node is labeled by the sign of the corresponding literal in the clause. A resolution is represented by unifying two atom nodes of different clause trees which represent complementary literals. The merge of two identical literals is represented by placing the path joining the two corresponding atom nodes into the set \(M\) of chosen merge paths. The tail of the merge path becomes a closed leaf, while the head remains an open leaf which can be resolved on. The clause \(cl(T)\) that \(T\) represents is the set of literals corresponding to the labels of the open leaves modified by the signs of the incident edges. The fundamental purpose of a clause tree \(T\) is to show that \(cl(T)\) can be derived from \(S\) using resolution.
Loveland’s model elimination ME, the selected literal procedure SL, and Shostak’s graph construction procedure GC are explained in a unified manner using clause trees. The condition required for choosing a merge path whose head is not a leaf is given. This allows a clause tree to be built in one way (the build ordering) but justified as a proof in another (the proof ordering).
The ordered clause set restriction and the foothold score restriction are explained using the operation on clause trees of merge path reversal. A new procedure called ALPOC, which combines ideas from ME, GC and Spencer’s ordered clause set restriction (OC), to form a new procedure tighter than any of the top down procedures above, is developed and shown to be sound and complete.
Another operation on clause trees called surgery is defined, and used to define a minimal clause tree. Any non-minimal clause tree can be reduced to a minimal clause tree using surgery, thereby showing that non-minimal clause trees are redundant. A sound procedure MinALPOC that produces only minimal clause trees is given. Mergeless clause trees are shown to be equivalent to each of input resolution, unit resolution and relative Horn sets, thereby giving short proofs of some known results. Many other new proof procedures using clause trees are discussed briefly, leaving many open questions.

MSC:

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

METEOR; SETHEO; TPTP; OTTER
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andrews, P. B., Refutations by matings, IEEE Trans. Comput., 25, 801-807 (1976) · Zbl 0331.68050
[2] Astrachan, O. L.; Loveland, D. W., METEORs: high performance theorem provers using model elimination, (Boyer, R. S., Automated Reasoning: Essays in Honor of Woody Bledsoe (1991), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht) · Zbl 0882.68132
[3] Astrachan, O. L.; Stickel, M., Caching and lemmaizing in model elimination theorem provers, (Kapur, D., Automated Deduction— CADE-11. Automated Deduction— CADE-11, Lecture Notes in Artificial Intelligence, 607 (1992), Springer: Springer Berlin), 224-238, Saratoga Springs
[4] Bibel, W., Short proof of the pigeonhole formulas based on the connection method, J. Autom. Reasoning, 6, 287-297 (1990) · Zbl 0702.68091
[5] Chang, C.-L.; Lee, R. C.-T., (Symbolic Logic and Mechanical Theorem Proving (1973), Academic Press: Academic Press New York) · Zbl 0263.68046
[6] Chvátal, V.; Szemerédi, E., Many hard examples for resolution, J. ACM, 35, 759-768 (1988) · Zbl 0712.03008
[7] Cook, S. A.; Reckhow, R. A., The relative efficiency of propositional proof systems, J. Symbolic Logic, 44, 36-50 (1979) · Zbl 0408.03044
[8] Eisinger, N., Completeness, Confluence and Related Properties of Clause Graph Resolution, (Research Notes in Artificial Intelligence (1991), Pittman: Pittman London), Morgan Kaufmann, San Mateo, CA
[9] Haken, A., The intractability of resolution, Theoret. Comput. Sci., 39, 297-308 (1985) · Zbl 0586.03010
[10] Harary, F., (Graph Theory (1969), Addison-Wesley: Addison-Wesley Reading, MA) · Zbl 0182.57702
[11] J.D. Horton and D. Sharpe, private communication.; J.D. Horton and D. Sharpe, private communication.
[12] Horton, J. D.; Spencer, B., A top down algorithm to find only minimal clause trees, (Dreschler-Fischer, L.; Pribbenow, S., KI-95 Activities: Workshops, Posters, Demos. KI-95 Activities: Workshops, Posters, Demos, Bielefeld (1995), Gesellschaft für Informatik: Gesellschaft für Informatik Bonn), 79-80
[13] Horton, J. D.; Spencer, B., Reducing search with minimal clause trees, (Tech. Rept. TR95-099 (1995), Faculty of Computer Science, University of New Brunswick: Faculty of Computer Science, University of New Brunswick Fredericton, NB, Canada)
[14] Horton, J. D.; Spencer, B., Bottom-up procedures for minimal clause trees, (Tech. Rept. TR96-101 (1996), Faculty of Computer Science, University of New Brunswick: Faculty of Computer Science, University of New Brunswick Fredericton, NB, Canada)
[15] Hynes, R., The disequality strategy in theorem proving, (undergraduate thesis (1995), Faculty of Computer Science, University of New Brunswick: Faculty of Computer Science, University of New Brunswick Fredericton, NB, Canada)
[16] Kowalski, R.; Kuehner, D., Linear resolution with selection function, Artif. Intell., 2, 227-260 (1971) · Zbl 0234.68037
[17] Letz, R.; Mayr, K.; Goller, C., Controlled integration of the cut rule into connection tableau calculi, J. Autom. Reasoning, 13, 297-337 (1994) · Zbl 0816.03005
[18] Letz, R.; Shumann, J.; Bayerl, S.; Bibel, W., SETHEO: a high-performance theorem prover, J. Autom. Reasoning, 8, 183-212 (1992) · Zbl 0759.68080
[19] Lobo, J.; Miner, J.; Rajasekar, A., (Fundamentals of Disjunctive Logic Programming (1992), MIT Press: MIT Press Boston)
[20] Loveland, D. W., Mechanical theorem proving by model elimination, J. ACM, 15, 236-251 (1968) · Zbl 0162.02804
[21] Loveland, D. W., (Automated Theorem Proving: A Logical Basis (1978), North-Holland: North-Holland Amsterdam) · Zbl 0364.68082
[22] McCune, W. W., OTTER 2.0 users guide, (Tech. Rept. ANL-90/9 (1990), Mathematics and Computer Science Division, Argonne National Laboratories: Mathematics and Computer Science Division, Argonne National Laboratories Argonne, IL)
[23] Minker, J.; Zanon, G., An extension to linear resolution with selection function, Inform. Process. Lett., 14, 191-194 (1982) · Zbl 0477.68100
[24] Murray, N. V.; Rosenthal, E., Dissolution: making paths vanish, J. ACM, 40, 504-535 (1993) · Zbl 0785.68083
[25] Reiter, R., Two results on ordering for resolution with merging and linear format, J. ACM, 18, 630-646 (1971) · Zbl 0238.68030
[26] Robinson, J. A., A machine-oriented logic based on the resolution principle, J. ACM, 12, 23-41 (1965) · Zbl 0139.12303
[27] Sharpe, D., AllPaths theorem prover, (Undergraduate thesis (1995), Faculty of Computer Science, University of New Brunswick: Faculty of Computer Science, University of New Brunswick Fredericton, NB, Canada)
[28] Sharpe, D., Backwards basic factoring: a pessimistic analog of basic factoring, (Stewman, J., Proceedings of the Ninth Florida Artificial Intelligence Research Symposium. Proceedings of the Ninth Florida Artificial Intelligence Research Symposium, Key West, FL (1996)), 459-462
[29] Shostak, R. E., Refutation graphs, Artif. Intell., 7, 51-64 (1976) · Zbl 0328.68080
[30] Spencer, B., Linear resolution with ordered clauses, (Lobo, J.; Loveland, D.; Rajasekar, A., Proceedings ILPS Workshop—Disjunctive Logic Programming. Proceedings ILPS Workshop—Disjunctive Logic Programming, San Diego, CA (1991))
[31] Spencer, B., The ordered clause restriction of model elimination and SLI resolution, (Miller, D., Proceedings International Symposium of Logic Programming. Proceedings International Symposium of Logic Programming, Vancouver, BC (1993)), 678
[32] Spencer, B., Avoiding duplicate proofs with the foothold refinement, Ann. Math. Artif. Intell., 12, 117-140 (1994) · Zbl 0858.68091
[33] Spencer, B.; Horton, J. D.; Francis, K., Experiments with the ALPOC theorem prover, (Tech. Rept. TR95-094 (1995), Faculty of Computer Science, University of New Brunswick: Faculty of Computer Science, University of New Brunswick Fredericton, NB, Canada)
[34] Stickel, M., A Prolog technology theorem prover: implementation by an extended Prolog compiler, J. Autom. Reasoning, 1, 353-380 (1988) · Zbl 0662.68104
[35] Stickel, M., A Prolog technology theorem prover: a new exposition and implementation in Prolog, Theor. Comput. Sci., 104, 109-128 (1992) · Zbl 0771.68096
[36] M. Stickel, personal communication.; M. Stickel, personal communication.
[37] Stickel, M., Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction, J. Autom. Reasoning, 13, 189-210 (1994) · Zbl 0819.68113
[38] Sutcliffe, G.; Suttner, C.; Yemenis, T., The TPTP problem library, (Kapur, D., Automated Deduction—CADE-12. Automated Deduction—CADE-12, Nancy. Automated Deduction—CADE-12. Automated Deduction—CADE-12, Nancy, Lecture Notes in Artificial Intelligence, 814 (1994), Springer: Springer Berlin), 252-266 · Zbl 1433.68569
[39] Tseitin, G. S., On the complexity of derivations in prepositional calculus, (Stisenko, A. O., Studies in Mathematics and Mathematical Logic Part II (1970), Consultants Bureau: Consultants Bureau New York), 115-125
[40] Wos, L., (Automated Reasoning: 33 Basic Research Problems (1988), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ) · Zbl 0663.68102
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.