Skip to main content
SpringerLink
Log in

Hyper resolution and equality axioms without function substitutions

  • Conference paper
  • First Online:
10th International Conference on Automated Deduction (CADE 1990)

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

Included in the following conference series:

  • 165 Accesses

Abstract

When hyperresolution used with equality axioms, the function substitution axioms tend to produce myriads of new clauses whenever a positive equality literal is present. The analogue for paramodulation is the large number of potential paramodulants where the “into” term is not at the top level of its literal.

In this study, we will prove that for some class of clause sets, the use of function substitution axioms can be eliminated. Analogously, paramodulation can be applied to the top level terms only.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Kowalski, R. The Case for Using Equality Axioms in Automatic Demonstration. Symposium on Automatic Demonstration, Paris, 1969.

    Google Scholar 

  2. McCune, W., Henschen, L. Semantic paramodulation for horn sets. Proceedings of the 8th Int. Joint Conference on AI, pp 902–908, Karlsruhe, W. Germany, 1983.

    Google Scholar 

  3. Ozturk, Y. Interactive Advice System for Automated Theorem Provers. Ph.D. Thesis, EECS Department, Northwestern University, Evanston, 1989.

    Google Scholar 

  4. Wos, L., Carson, D., and Robinson, G. Efficiency and completeness of the set-of-support strategy in theorem proving. Journal of the ACM 12, pp 536–541, 1965.

    Google Scholar 

  5. Wos, L., Overbeek, R., Lusk, E., Boyle, J. Automated Reasoning: Introduction and Applications. Prentice-Hall, Inc., New Jersey 1984.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Electrical Engineering and Computer Science Department, Northwestern University, 60208, Evanston, IL, U.S.A.

    Yusuf Ozturk & Lawrence Henschen

Authors
  1. Yusuf Ozturk
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lawrence Henschen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mark E. Stickel

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ozturk, Y., Henschen, L. (1990). Hyper resolution and equality axioms without function substitutions. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_107

Download citation

  • DOI: https://doi.org/10.1007/3-540-52885-7_107

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52885-2

  • Online ISBN: 978-3-540-47171-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation