Skip to main content
SpringerLink
Log in

Ordered Resolution vs. Connection Graph resolution

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2001)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2083))

Included in the following conference series:

Abstract

Connection graph resolution (cg-resolution) was introduced by Kowalski as a means of restricting the search space of resolution. Several researchers expected unrestricted connection graph (cg) resolution to be strongly complete until Eisinger proved that it was not. In this paper, ordered resolution is shown to be a special case of cg-resolution, and that relationship is used to prove that ordered cg-resolution is strongly complete. On the other hand, ordered resolution provides little insight about completeness of first order cg-resolution and little about the establishment of strong completeness from completeness. A first order version of Eisinger’s cyclic example is presented, illustrating the difficulties with first order cg resolution. But resolution with selection functions does yield a simple proof of strong cg-completeness for the unit-refutable class.

Acknowledgement

Bernhard Beckert noticed an error in an earlier version and gave several useful and simplifying suggestions. A discussion with Harald Ganzinger helped clarify several issues.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bachmair, L. and Ganzinger, H. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.

    Article  MathSciNet  MATH  Google Scholar 

  2. Beckert, B. and Hähnle, R. Analytic tableaux. In W. Bibel and P. Schmitt, editors, Automated Deduction: A Basis for Applications, volume I, chapter 1, pp. 11–41. Kluwer, 1998.

    Google Scholar 

  3. Bibel, W. On matrics with connections. JACM, 28:633–645, 1981.

    Article  MathSciNet  MATH  Google Scholar 

  4. Bibel, W. and Eder, E. Decomposition of tautologies into regular formulas and strong completeness of connection graph resolution. Journal of the ACM, 44(2): 320–344, 1997.

    Article  MathSciNet  MATH  Google Scholar 

  5. de Nivelle, Hans. Ordering Refinements of Resolution. Ph.D. Thesis, Technische Universiteit Delft.

    Google Scholar 

  6. Dershowitz, N. Termination of rewriting. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, pages 69–115. Academic Press, 1987. Reprinted from Journal of Symbolic Computation.

    Google Scholar 

  7. Eisinger, N. Completeness, confluence, and related properties of clause graph resolution. Research notes in artificial intelligence. Pitman Publishing, 1991.

    Google Scholar 

  8. Joyner, W.H. Resolution strategies as decision procedures. J. ACM 23,1 (July 1976), 398–417.

    Article  MathSciNet  MATH  Google Scholar 

  9. Kowalski, R. and Hayes, P.J. Semantic trees in automatic theorem proving. In Machine Intelligence, volume 4, pages 87–101. Edinburgh University Press, 1969. Reprinted in [17].

    MathSciNet  MATH  Google Scholar 

  10. Kowalski, R. A proof procedure using connection graphs. Journal of the ACM, 22(4):572–595, 1975.

    Article  MathSciNet  MATH  Google Scholar 

  11. Loveland, D.W., Automated Theorem Proving: A Logical Basis, North-Holland, New York (1978).

    Google Scholar 

  12. Murray, N.V. and Rosenthal, E. Dissolution: Making paths vanish. Journal of the ACM, 40(3):504–535, 1993.

    Article  MathSciNet  MATH  Google Scholar 

  13. Reynolds, J. Unpublished seminar notes, Stanford University, Palo Alto, CA, 1966.

    Google Scholar 

  14. Robinson, J.A., Automatic deduction with hyper-resolution, International Journal of Computer Mathematics, 1 (1965), 227–234.

    MathSciNet  MATH  Google Scholar 

  15. Sibert, E.E., A machine-oriented logic incorporating the equality relation, Machine Intelligence 4 (Meltzer and Michie, eds.), Edinburgh University Press, Edinburgh, 1969, 103–133.

    Google Scholar 

  16. Siekmann, J. and Stephan, W. Completeness and soundness of the connection graph procedure. Interner Bericht 7/76, Institut I, Fakultät für Informatik, Universitüt Karlsruhe, 1976.

    Google Scholar 

  17. Siekmann, J. and Wrightson, G., editors.Automation of Reasoning: Classical Papers in Computational Logic 1967–1970, volume 2. Springer-Verlag, 1983.

    Google Scholar 

  18. Siekmann, J. and Wrightson, G., editors. Automation of Reasoning: Classical Papers in Computational Logic 1957–1966, volume 1. Springer-Verlag, 1983.

    Google Scholar 

  19. Siekmann, J. and Wrightson, G. Erratum: a counterexample to W. Bibel’s and E. Eder’s strong completeness results for connection graph resolution. Journal of the ACM, to appear.

    Google Scholar 

  20. Wos, L., Carson, D., and Robinson, G.A. The unit preference strategy in theorem proving. In Fall Joint Computer Conference, AFIPS, Washington D.C., pages 615–621. Spartan Books, 1964. Reprinted in [18].

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computing Science, Chalmers University of Technology, S-41296, Gothenburg, Sweden

    Reiner Hähnle

  2. Department of Computer Science, State University of New York, Albany, NY, 12222, USA

    Neil V. Murray

  3. Department of Mathematics, University of New Haven, West Haven, CT, 06516, USA

    Erik Rosenthal

Authors
  1. Reiner Hähnle
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Neil V. Murray
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Erik Rosenthal
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Automated Reasoning Project and Department of Computer Science, Australian National University, Canberra, ACT, 0200, Australia

    Rajeev Goré

  2. AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Favoritenstr. 9, E185-2, 1040, Wien, Austria

    Alexander Leitsch

  3. Institut für Informatik, Technische Universität München, 80290, München, Germany

    Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hähnle, R., Murray, N.V., Rosenthal, E. (2001). Ordered Resolution vs. Connection Graph resolution. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-45744-5_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42254-9

  • Online ISBN: 978-3-540-45744-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation