Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Computer Science Logic

CSL 1994: Computer Science Logic pp 279–293Cite as

Resolution games and non-liftable resolution orderings

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 933))

Abstract

We prove the completeness of the combination of ordered resolution and factoring for a large class of non-liftable orderings, without the need for any additional rules like saturation. This is possible because of a new proof method wich avoids making use of the standard ordered lifting theorem. This proof method is based on resolution games.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Baumgartner, An ordered theory calculus, in LPAR92, Springer Verlag, Berlin, 1992.

    Google Scholar 

  2. L. Bachmair, H. Ganzinger, On restrictions of ordered paramodulation with simplification, CADE 10, pp 427–441, Keiserslautern, Germany, Springer Verlag, 1990.

    Google Scholar 

  3. M. Bezem, Completeness of resolution revisited, Theoretical computer science 74, pp. 227–237, 1990.

    Article  Google Scholar 

  4. R.S. Boyer, Locking: A restriction of resolution, Ph. D. Thesis, University of Texas at Austin, Texas 1971.

    Google Scholar 

  5. C-L. Chang, R.C-T. Lee, Symbolic logic and mechanical theorem proving, Academic Press, New York 1973.

    Google Scholar 

  6. C. Fermüller, A. Leitsch, T. Tammet, N. Zamov, Resolution methods for the decision problem, Springer Verlag, 1993.

    Google Scholar 

  7. W.H. Joyner, Resolution Strategies as Decision Procedures, J. ACM 23, 1 (July 1976), pp. 398–417.

    Article  Google Scholar 

  8. R. Kowalski, P.J. Hayes, Semantic trees in automated theorem proving, Machine Intelligence 4, B. Meltzer and D. Michie, Edingburgh University Press, Edingburgh, 1969.

    Google Scholar 

  9. H. de Nivelle, Resolution games and non-liftable resolution orderings, Internal report 94-36, Department of Mathematics and Computer Science, Delft University of Technology.

    Google Scholar 

  10. J.A. Robinson, A machine oriented logic based on the resolution principle, Journal of the ACM, Vol. 12, pp 23–41, 1965.

    Article  Google Scholar 

  11. T. Tammet, Seperate orderings for ground and non-ground literals preserve completeness of resolution, unpublished, 1994.

    Google Scholar 

  12. N.K. Zamov: On a Bound for the Complexity of Terms in the Resolution Method, Trudy Mat. Inst. Steklov 128, pp. 5–13, 1972.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, Delft University of Technology, Julianalaan 132, 2628, BL, the Netherlands

    Hans de Nivelle

Authors
  1. Hans de Nivelle
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Leszek Pacholski Jerzy Tiuryn

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Nivelle, H. (1995). Resolution games and non-liftable resolution orderings. In: Pacholski, L., Tiuryn, J. (eds) Computer Science Logic. CSL 1994. Lecture Notes in Computer Science, vol 933. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022263

Download citation

  • DOI: https://doi.org/10.1007/BFb0022263

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60017-6

  • Online ISBN: 978-3-540-49404-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation