A resolution decision procedure for the guarded fragment

  • Hans de Nivelle
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


We give a resolution based decision procedure for the guarded fragment of [ANB96]. The relevance of the guarded fragment lies in the fact that many modal logics can be translated into it. In this way the guarded fragment acts as a framework explaining the nice properties of these modal logics. By constructing an effective decision procedure for the guarded fragment we define an effective procedure for deciding these modal logics.


Modal Logic Decision Procedure Ground Term Modal Formula Existential Quantifier 
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. [ANB96]
    H. Andréka, J. van Benthem, I. Németi, Modal Languages and Bounded Fragments of Predicate Logic, ILLC Research Report ML-96-03, 1996.Google Scholar
  2. [BFL94]
    M. Baaz, C. Fermüller, A. Leitsch, A Non-Elementary Speed Up in Proof Length by Structural Clause Form Transformation, In LICS 94.Google Scholar
  3. [BL94]
    M. Baaz, A. Leitsch, On Skolemization and Proof Complexity, Fundamenta Informatica, Vol. 20–4, 1994.Google Scholar
  4. [Benthem96]
    J. van Benthem, Exploring Logical Dynamics, CSLI Publications, Stanford, California USA, 1996.Google Scholar
  5. [Benthem97]
    J. van Benthem, Dynamic Bits and Pieces, LP-97-01, Research Report of the Institute for Logic, Language and Information, 1997.Google Scholar
  6. [BGG96]
    E. Börger, E. GrÄdel, Y. Gurevich, The Classical Decision Problem, Springer Verlag, Berlin Heidelberg, 1996.Google Scholar
  7. [Catach91]
    L. Catach, TABLEAUX, a general theorem prover for modal logics, Journal of automated reasoning 7, pp. 489–510, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  8. [CL73]
    C-L. Chang, R. C-T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973.Google Scholar
  9. [DG79]
    B. Dreben, W.D. Goldfarb, The Decision Problem, Solvable Classes of Quantificational Formulas, Addision-Wesley Publishing Company, Inc. 1979.Google Scholar
  10. [EnjFar89]
    P. Enjalbert, L. Fariñas del Cerro, Modal resolution in clausal form, Theoretical Computer Science 65, 1989.Google Scholar
  11. [FarHerz88]
    L. Fariñas del Cerro and A. Herzig, linear modal deductions, CADE '88, pp. 487–499, 1988.Google Scholar
  12. [FLTZ93]
    C. Fermüller, A. Leitsch, T. Tammet, N. Zamov, Resolution Methods for the Decision Problem, Lecture Notes in Artificial Intelligence 679, Springer Verlag, 1993.Google Scholar
  13. [Fitting88]
    M. Fitting, First-order modal tableaux, Journal of automated resoning 4, pp. 191–213, 1991.MathSciNetGoogle Scholar
  14. [Fitting91]
    M. Fitting, Destructive Modal Resolution, Journal of Logic and Computation, volume 1, pp. 83–97, 1990.zbMATHMathSciNetGoogle Scholar
  15. [Foret92]
    A. Foret, Rewrite rule systems for modal propositional logic, Journal of logic programming 12, pp. 281–298, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  16. [Graedel97]
    E. GrÄdel, On the Restraining Power of Guards, manuscript, 1997.Google Scholar
  17. [Joyner76]
    W. H. Joyner, Resolution Strategies as Decision Procedures, J. ACM 23, 1 (July 1976),1 pp. 398–417, 1976.zbMATHCrossRefMathSciNetGoogle Scholar
  18. [Ladner77]
    R.E. Ladner, The computational complexity of provability in systems of modal propositional logic, SIAM Journal on Computing 6, pp 467–480, 1977.zbMATHCrossRefMathSciNetGoogle Scholar
  19. [McCune95]
    W. W. McCune, Otter 3.0 Reference Manual and Guide, Argonne National Laboratory, Mathematics and Computer Science Division, can be obtained from, directory pub/Otter, 1995.Google Scholar
  20. [Nivelle92]
    H. de Nivelle, Generic modal resolution, Technical Report 92-90, Delft University of Technology, fac. TWI, 1992.Google Scholar
  21. [Nivelle93]
    Generic Resolution in Propositional Modal Systems, in LPAR 93, Springer Verlag Berlin, 1993.Google Scholar
  22. [Nivelle94]
    Resolution Games and Non-Liftable Resolution Orderings, in CSL 94, pp. 279–293, Springer Verlag, 1994.Google Scholar
  23. [Nivelle95]
    H. de Nivelle, Ordering Refinements of Resolution, Ph. D. Thesis, Delft University of Technology, 1995.Google Scholar
  24. [Nivelle98]
    H. de Nivelle, Resolution Decides the Guarded Fragment, ILLC-Report CT-1998-01, 1998.Google Scholar
  25. [Ohlbach88a]
    H.J. Ohlbach, A resolution calculus for modal logics, PhD thesis, UniversitÄt Kaiserslautern, 1988.Google Scholar
  26. [Ohlbach88b]
    H.J. Ohlbach, A resolution calculus for modal logics, CADE '88, pp. 500–516, 1988.Google Scholar
  27. [OWbach95]
    H-J. Ohlbach, C. Weidenbach, A note on Assumptions About Skolem Functions, Journal of Automated Reasoning 15, Vol. 2, pp. 267–275, 1995.CrossRefMathSciNetGoogle Scholar
  28. [Robinson65]
    J. A. Robinson, A Machine Oriented Logic Based on the Resolution Principle, Journal of the ACM, Vol. 12. pp. 23–41, 1965zbMATHCrossRefGoogle Scholar
  29. [ATP97]
    The CADE-13 Automated Theorem Proving System Competition, Journal of Automated Reasoning Special Issue, Vol. 18, No. 2, Edited by G. Sutcliffe and C. Suttner, 1996.Google Scholar
  30. [Tammet90]
    T. Tammet, The Resolution Program, Able to Decide some Solvable Classes, in COLOG-88, Springer LNCS, pp. 300–312, 1990.Google Scholar
  31. [Wbach96]
    C. Weidenbach, (Max-Planck-Institut für Informatik), The Spass & Flotter Users Guide, Version 0.55, can be obtained from, directory pub/SPASS, 1997.Google Scholar
  32. [Zamov72]
    N.K. Zamov, On a Bound for the Complexity of Terms in the Resolution Method, Trudy Mat. Inst. Steklov 128, pp. 5–13, 1972.MathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Hans de Nivelle
    • 1
  1. 1.Centrum voor Wiskunde en InformaticaGB AmsterdamThe Netherlands

Personalised recommendations