Resolution Games and Non-Liftable Resolution Orderings

  • Hans de Nivelle
Part of the Collegium Logicum book series (COLLLOGICUM, volume 2)


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, as for example saturation. This is possible because of a new proof method which avoids making use of the standard ordered lifting theorem. This new proof method is based on a new technique, which we call the resolution game.


Function Symbol Predicate Symbol Winning Strategy Derivation Tree Ground Instance 
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. [Boyer7l]
    R.S. Boyer, Locking: A Restriction of Resolution, Ph. D. Thesis, University of Texas at Austin, Texas 1971.Google Scholar
  2. [ChangLee73]
    C-L. Chang, R. C-T. Lee, Symbolic logic and mechanical theorem proving, Academic Press, New York 1973.MATHGoogle Scholar
  3. [Egly]
    On Definitional Transformations to Normal Form for Intuitionistic Logic, unpublished.Google Scholar
  4. [FLTZ93]
    C. Fermüller, A. Leitsch, T. Tammet, N. Zamov, Resolution Methods for the Decision Problem, Springer Verlag, 1993.Google Scholar
  5. [Galllier86]
    Jean H. Gallier, Logic for Computer Science, (Foundations of Automatic Theorem Proving), Harper & Row, Publishers, New York, 1986.Google Scholar
  6. [Girard87]
    Linear Logic, in Theoretical Computer Science 50, pages 1–102, 1987.Google Scholar
  7. [HR91]
    J. Hsiang and M. Rusinowitch, Proving Refutational Completeness of Theorem-Proving Strategies: The Transfinite Semantic Tree Method, Journal of the ACM, Vol. 38, no. 3, July 1991, pp. 559–587.MathSciNetMATHCrossRefGoogle Scholar
  8. [Joy76]
    W.H. Joyner, Resolution Strategies as Decision Procedures, J. ACM 23, 1 (July 1976), pp. 398–417.MathSciNetMATHCrossRefGoogle Scholar
  9. [KH69]
    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
  10. [Leitsch88]
    A. Leitsch, On Some Formal Problems in Resolution Theorem Proving, Yearbook of the Kurt Gödel Society, pp. 35–52, 1988.Google Scholar
  11. [Lovelnd78]
    D. W. Loveland, Automated Theorem Proving, a Logical Basis, North Holland Publishing Company, Amsterdam, New York, Oxford, 1978.Google Scholar
  12. [Mints88]
    G. Mints, Gentzen-Type Systems and Resolution Rules, Part 1, Propositional Logic, in COLOG-88, International Conference on Computational Logic, Talinn (at that time) USSR, 1988.Google Scholar
  13. [Nivelle94a]
    H. de Nivelle, Resolution Games and Non-Liftable Resolution Orderings, Internal Report 94–36, Department of Mathematics and Computer Science, Delft University of Technology, 1994.Google Scholar
  14. [Nivelle94b]
    H. de Nivelle, Application of Resolution Games to Resolution Decision Procedures, Internal Report 94–50, Department of Mathematics and Computer Science, Delft University of Technology, 1994.Google Scholar
  15. [Nivelle95]
    Resolution Games and Non-Liftable Resolution Orderings, in CSL 94, pp 279–293, Springer Verlag, Kazimierz, Poland, 1994Google Scholar
  16. [Reynolds66]
    J. Reynolds, Unpublished Seminar Notes, Stanford University, Palo Alto, California, 1966.Google Scholar
  17. [Robins65]
    J.A. Robinson, A Machine Oriented Logic Based on the Resolution Principle, Journal of the ACM, Vol. 12, pp 23–41, 1965.MATHCrossRefGoogle Scholar
  18. [Stat79]
    R. Statman, Lower Bounds on Herbrand’s Theorem, in Proceedings of the American Mathematical Society, Vol. 75, Number 1, 1979.Google Scholar
  19. [Tamm93]
    T Tammet, Proof Search Strategies in Linear Logic, Report 70, Programming Methodology Group, Department of Computer Sciences, Chalmers University of Technology and University of Göteburg, 1993.Google Scholar
  20. [Tamm94]
    T Tammet, Separate Orderings for Ground and Non-Ground Literals Preserve Completeness of Resolution, unpublished, 1994.Google Scholar
  21. [Zam72]
    N.K. Zamov: On a Bound for the Complexity of Terms in the Resolution Method, Trudy Mat. Inst. Steklóv 128, pp. 5–13, 1972.MathSciNetGoogle Scholar

Copyright information

© Springer-Verlag/Wien 1996

Authors and Affiliations

  • Hans de Nivelle
    • 1
  1. 1.Department of Mathematics and Computer ScienceDelft University of Technologythe Netherlands

Personalised recommendations