Skip to main content
SpringerLink
Log in

Refinement Theorems in Resolution Theory

  • Chapter
Automation of Reasoning

Part of the book series: Symbolic Computation ((1064))

  • 557 Accesses

Abstract

The paper discusses some basic refinements of the Resolution Principle which are intended to improve the speed and efficiency of theorem-proving programs based on this rule of inference. It is proved that two of the refinements preserve the logical complete­ness of the proof procedure when used separately, but not when used in conjunction. The results of some preliminary experiments with the refinements are given.

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. Andrews, P. B., “Resolution with Merging”, JACM,15, No. 3, pp. 367–381, July 1968.

    Google Scholar 

  2. Luckham, D., “The Resolution Principle in Theorem-Proving”, Machine Intelligence 1, Collins and Michie (Eds), American Elsevier Inc., New York, 1967.

    Google Scholar 

  3. Luckham, D., “Some Tree-Paring Strategies for Theorem-Proving”, Machine Intelligence 3 D. Michie (Ed), Edinburgh University Press, pp. 95–112, 1968.

    Google Scholar 

  4. Robinson, J. A., “A Machine-Oriented Logic Based on the Resolution Principle”, JACM, 12, No. 1, pp. 23–41, January 1965.

    Google Scholar 

  5. Robinson, J. A., “Automatic Deduction with Hyper-Resolution”, International Journal of Computer Mathematics Vol. 1, pp. 227–234, 1965.

    MATH  Google Scholar 

  6. Slagle, J. R., “Automatic Theorem-Proving with Renamable and Semantic Resolution”, JACM, 14, pp. 687–697, October 1967.

    Google Scholar 

  7. Wos, L., Robinson, G., Carson, D., “Efficiency and Completeness of the Set of Support Strategy in Theorem Proving”, JACM,12, No. 4, pp. 536–541, October 1965.

    MathSciNet  Google Scholar 

  8. Wos, L., Robinson, G., Carson, D., Shelia, L., “The Concept of Demodulation in Theorem-Proving”, JACM 14, No. 4, pp. 698–704.

    Google Scholar 

  9. Wos, L., and Robinson, G., “The Maximal Model Theorem”, Abstract, Spring 1968 meeting of Association for Symbolic Logic, to appear in J. Symb. Logic.

    Google Scholar 

Download references

Authors
  1. D. Luckham
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik I, Universität Karlsruhe, Postfach 6380, D-7500, Karlsruhe, West Germany

    Jörg H. Siekmann

  2. Department of Information Science, Victoria University, Wellington, New Zealand

    Graham Wrightson

Rights and permissions

Reprints and permissions

Copyright information

© 1983 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Luckham, D. (1983). Refinement Theorems in Resolution Theory. In: Siekmann, J.H., Wrightson, G. (eds) Automation of Reasoning. Symbolic Computation. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-81955-1_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-81955-1_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-81957-5

  • Online ISBN: 978-3-642-81955-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation