Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution

ABSTRACT

This paper addresses and answers a fundamental question about resolution. Informally, what is gained with respect to the search for a proof by performing a single resolution step? It is first shown that any unsatisfiable formula may be decomposed into regular formulas provable in linear time (by resolution). A relevant resolution step strictly reduces at least one of the formulas in the decomposition while an irrelevant one does not contribute to the proof in any way. the relevance of this insight into the nature of resolution and of the unsatisfiability problem for the development of proof strategies and for complexity considerations are briefly discussed.The decomposition also provides a technique for establishing completeness proofs for refinements of resolution. As a first application, connection-graph resolution is shown to be strongly complete. This settles a problem that remained open for two decades despite many proff attempts. The result is relevant for theorem proving because without strong completeness a connection graph resolution prover might run into an infinite loop even on the ground level.

REFERENCES

• 1: Robert Anderson , W. W. Bledsoe, A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness, Journal of the ACM (JACM), v.17 n.3, p.525-534, July 1970 [doi>10.1145/321592.321603]
• 2: W. Bibel , E. Eder, Methods and calculi for deduction, Handbook of logic in artificial intelligence and logic programming (vol. 1), Oxford University Press, Inc., New York, NY, 1993
• 3: Wolfgang Bibel, On Matrices with Connections, Journal of the ACM (JACM), v.28 n.4, p.633-645, Oct. 1981 [doi>10.1145/322276.322277]
• 4: Wolfgang Bibel, On the Completeness of Connection Graph Resolution, Proceedings of the German Workshop on Artificial Intelligence, p.246-247, January 26-31, 1981
• 5: Wolfgang Bibel, Matings in matrices, Communications of the ACM, v.26 n.11, p.844-852, Nov. 1983 [doi>10.1145/182.183]
• 6: BIBEL, W. 1991. Perspectives on automated deduction. In Automated Reasoning: Essays in Honor of Woody Bledsoe. R. S. Boyer, ed. Kluwer Academic, Utrecht, Germany, pp. 77-104.
• 7: BIBEL, W. 1993. Deduction: Automated Logic. Academic Press, Orlando, Fla.
• 8: BROWN, F. M. 1976. Notes on chains and connection graphs. Personal notes. University of Edinburgh, Edinburgh, Scotland.
• 9: Chin-Liang Chang , Richard C. Lee , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
• 10: Vašek Chvátal , Endre Szemerédi, Many hard examples for resolution, Journal of the ACM (JACM), v.35 n.4, p.759-768, Oct. 1988 [doi>10.1145/48014.48016]
• 11: EISINGER, N. 1989. Completeness, Confluence, and Related Properties of Clause Graph Resolution. Ph.D. dissertation, Universitfit Kaiserslautern.
• 12: Dov M. Gabbay, Algorithmic Proof with Diminishing Resources, Part 1, Proceedings of the 4th Workshop on Computer Science Logic, p.156-173, October 01-05, 1990
• 13: GOLDFARB, W. D., ED. 1971. J.J. Herbrand--Logical writings. Reidel, Dordrecht, Germany.
• 14: Armin Haken, The intractability of resolution (complexity), 1984
• 15: HERBRAND, J.J. 1930. Recherches sur la thdorie de la ddmonstration. Travaux Soc. Sciences et Lettres Varsovie, C1. 3 (Mathem., Phys.), pp. 128. (English translation in Goldfarb {1971}.)
• 16: KOWALSKI, R., AND HAYES, P.J. 1969. Semantic trees in automated theorem proving. In Machine Intelligence 4, B. Meltzer and D. Michie, eds. Edinburgh University Press, Edinburgh, Scotland, pp. 87-101. (Also published in Siekmann and Wrightson {1983}, pp. 217-232.)
• 17: Robert Kowalski, A Proof Procedure Using Connection Graphs, Journal of the ACM (JACM), v.22 n.4, p.572-595, Oct. 1975 [doi>10.1145/321906.321919]
• 18: Stefan Klingenbeck , Reiner Hähnle, Semantic Tableaux with Ordering Restrictions, Proceedings of the 12th International Conference on Automated Deduction, p.708-722, June 26-July 01, 1994
• 19: N. J. Nilsson, Principles of artificial intelligence, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1980
• 20: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 21: ROBINSON, J. A. 1968. The generalized resolution principle. In Machine Intelligence 3, Donald Michie, ed. Edinburgh University Press, Edinburgh, Scotland, pp. 77-93. (Also published in Siekmann and Wrightson {1983}, pp. 135-151.)
• 22: ROBINSON, J.A. 1995. A sketch of the Property A view of things. Technical Univ., Darmstadt, Germany.
• 23: SELMAN, B., AND KAUTZ, H. 1993. Domain-independent extensions to gsat: Solving large structured satisfiability problems. In HCAI-93--Proceedings of the 13th International Joint Conference on Artificial Intelligence. Ruzena Bajcsy, ed. Morgan-Kaufmann, pp. 290-295.
• 24: SIEKMANN, J., AND WRIGHTSON, G., EDS. 1983. Automation of Reasoning--Classical Papers on Computational Logic 1967-1970, vol. 2. Springer, Berlin, Germany.
• 25: Gert Smolka, Completeness of the Connection Graph Proof Procedure for Unit-Refutable Clause Sets, Proceedings of the 6th German Workshop on Artificial Intelligence, p.191-204, September 27-October 01, 1982
• 26: TSEITIN, G.S. 1968/1970. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part H. A. O. Slisenko, ed. Seminars in Mathematics, V. A. Steklov Mathematical Institute, vol. 8. Leningrad, Russia, pp. 234-259. (English translation: Consultants Bureau, New York, 1970, pp. 115-125.) (Also published in Siekmann and Wrightson {1983}, pp. 466-483.)
• 27: Alasdair Urquhart, Hard examples for resolution, Journal of the ACM (JACM), v.34 n.1, p.209-219, Jan. 1987 [doi>10.1145/7531.8928]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Machine-independent complexity**

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

General Terms:
Algorithms, Theory

Keywords:
connection-graph resolution, decomposition of unsatisfiable formulas, regular graphs, semantic trees, strong completeness