A resolution decision procedure for the guarded fragment

1. 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. 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. M. Baaz, A. Leitsch, On Skolemization and Proof Complexity, Fundamenta Informatica, Vol. 20–4, 1994.

   Google Scholar 

4. J. van Benthem, Exploring Logical Dynamics, CSLI Publications, Stanford, California USA, 1996.

   Google Scholar 

5. J. van Benthem, Dynamic Bits and Pieces, LP-97-01, Research Report of the Institute for Logic, Language and Information, 1997.

   Google Scholar 

6. E. Börger, E. GrÄdel, Y. Gurevich, The Classical Decision Problem, Springer Verlag, Berlin Heidelberg, 1996.

   Google Scholar 

7. L. Catach, TABLEAUX, a general theorem prover for modal logics, Journal of automated reasoning 7, pp. 489–510, 1991.

   Article  MATH  MathSciNet  Google Scholar 

8. C-L. Chang, R. C-T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973.

   Google Scholar 

9. B. Dreben, W.D. Goldfarb, The Decision Problem, Solvable Classes of Quantificational Formulas, Addision-Wesley Publishing Company, Inc. 1979.

   Google Scholar 

10. P. Enjalbert, L. Fariñas del Cerro, Modal resolution in clausal form, Theoretical Computer Science 65, 1989.

    Google Scholar 

11. L. Fariñas del Cerro and A. Herzig, linear modal deductions, CADE '88, pp. 487–499, 1988.

    Google Scholar 

12. 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. M. Fitting, First-order modal tableaux, Journal of automated resoning 4, pp. 191–213, 1991.

    MathSciNet  Google Scholar 

14. M. Fitting, Destructive Modal Resolution, Journal of Logic and Computation, volume 1, pp. 83–97, 1990.

    MATH  MathSciNet  Google Scholar 

15. A. Foret, Rewrite rule systems for modal propositional logic, Journal of logic programming 12, pp. 281–298, 1992.

    Article  MATH  MathSciNet  Google Scholar 

16. E. GrÄdel, On the Restraining Power of Guards, manuscript, 1997.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

18. R.E. Ladner, The computational complexity of provability in systems of modal propositional logic, SIAM Journal on Computing 6, pp 467–480, 1977.

    Article  MATH  MathSciNet  Google Scholar 

19. W. W. McCune, Otter 3.0 Reference Manual and Guide, Argonne National Laboratory, Mathematics and Computer Science Division, can be obtained from ftp.mcs.anl.gov, directory pub/Otter, 1995.

    Google Scholar 

20. H. de Nivelle, Generic modal resolution, Technical Report 92-90, Delft University of Technology, fac. TWI, 1992.

    Google Scholar 

21. Generic Resolution in Propositional Modal Systems, in LPAR 93, Springer Verlag Berlin, 1993.

    Google Scholar 

22. Resolution Games and Non-Liftable Resolution Orderings, in CSL 94, pp. 279–293, Springer Verlag, 1994.

    Google Scholar 

23. H. de Nivelle, Ordering Refinements of Resolution, Ph. D. Thesis, Delft University of Technology, 1995.

    Google Scholar 

24. H. de Nivelle, Resolution Decides the Guarded Fragment, ILLC-Report CT-1998-01, 1998.

    Google Scholar 

25. H.J. Ohlbach, A resolution calculus for modal logics, PhD thesis, UniversitÄt Kaiserslautern, 1988.

    Google Scholar 

26. H.J. Ohlbach, A resolution calculus for modal logics, CADE '88, pp. 500–516, 1988.

    Google Scholar 

27. H-J. Ohlbach, C. Weidenbach, A note on Assumptions About Skolem Functions, Journal of Automated Reasoning 15, Vol. 2, pp. 267–275, 1995.

    Article  MathSciNet  Google Scholar 

28. J. A. Robinson, A Machine Oriented Logic Based on the Resolution Principle, Journal of the ACM, Vol. 12. pp. 23–41, 1965

    Article  MATH  Google Scholar 

29. 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. T. Tammet, The Resolution Program, Able to Decide some Solvable Classes, in COLOG-88, Springer LNCS, pp. 300–312, 1990.

    Google Scholar 

31. C. Weidenbach, (Max-Planck-Institut für Informatik), The Spass & Flotter Users Guide, Version 0.55, can be obtained from ftp.mpi-sb.mpg.de, directory pub/SPASS, 1997.

    Google Scholar 

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

    MathSciNet  Google Scholar 

Download references