Some Remarks on Completeness, Connection Graph Resolution, and Link Deletion

  • Reiner Hähnle
  • Neil V. Murray
  • Erik Rosenthal
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


A new completeness proof that generalizes the Anderson-Bledsoe excess literal argument is developed for connection-graph resolution. The technique also provides a simplified completeness proof for semantic resolution. Some observations about subsumption and about link deletion are made. Link deletion is the basis for connection graphs. Subsumption plays an important role in most resolution-based inference systems. In some settings—for example, connection graphs in negation normal form—both subsumption and link deletion can be quite tricky. Nevertheless, a completeness result that uses both is obtained in this setting.


Completeness Proof Disjunctive Normal Form Unit Clause Semantic Tree Resolution Step 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Anderson and W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. JACM, 17(3):525–534, July 1970.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    L. Bachmair and H. Ganzinger. A theory of resolution. Technical Report MPI-I-97-2-005, Max-Planck-Institut für Informatik, Saarbrücken, 1997. To appear in: J. A. Robinson & A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier.Google Scholar
  3. 3.
    W. Bibel. On matrices with connections. JACM, 28:633–645, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    W. Bibel and E. Eder. Decomposition of tautologies into regular formulas and strong completeness of connection graph resolution. JACM, 44(2):320–344, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. CACM, 5:394–397, 1962.zbMATHMathSciNetGoogle Scholar
  6. 6.
    R. Hähnle, N. Murray, and E. Rosenthal. Completeness for linear regular negation normal form inference systems. In Z. W. Raś and A. Skowron, editors, Found. of Intelligent Systems ISMIS’97, Charlotte/NC, USA, volume 1325 of LNCS, pages 590–599. Springer-Verlag, 1997.Google Scholar
  7. 7.
    R. Hähnle, N. Murray, and E. Rosenthal. A remark on proving completeness. In D. Galmiche, editor, Position Papers at Conf. on Analytic Tableaux and Related Methods, Nancy, France, pages 41–47, 1997. Tech. Rep. 97-R-030, CRIN Nancy.Google Scholar
  8. 8.
    R. Kowalski. A proof procedure using connection graphs. JACM, 22(4):572–595, 1975.zbMATHCrossRefGoogle Scholar
  9. 9.
    N. Murray, A. Ramesh, and E. Rosenthal. The semi-resolution inference rule and prime implicate computations. In Proc. Fourth Golden West International Conference on Intelligent Systems, San Fransisco, CA, USA, pages 153–158, June 1995.Google Scholar
  10. 10.
    N. V. Murray and E. Rosenthal. Inference with path resolution and semantic graphs. JACM, 34(2):225–254, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    N. V. Murray and E. Rosenthal. Dissolution: Making paths vanish. JACM, 40(3):504–535, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    J. A. Robinson. The generalized resolution principle. In Machine Intelligence, volume 3, pages 77–93. Oliver and Boyd, Edinburgh, 1968.Google Scholar
  13. 13.
    M. E. Stickel. A nonclausal connection-graph resolution theorem-proving program. In D. Waltz, editor, Proc. National Conference on Artificial Intelligence, pages 229–233, Pittsburgh, PA, Aug. 1982. AAAI Press.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Reiner Hähnle
    • 1
  • Neil V. Murray
    • 2
  • Erik Rosenthal
    • 3
  1. 1.Dept. of Computer ScienceUniv. of KarlsruheKarlsruheGermany
  2. 2.Dept. of Computer ScienceState Univ. of New YorkAlbanyUSA
  3. 3.Dept. of MathematicsUniv. of New HavenWest HavenUSA

Personalised recommendations