Decidability by resolution for many modal logics^{∗}

Renate A. Schmidt

Max-Planck-Institut für Informatik, Im Stadtwald 66123 Saarbrücken, Germany Email: schmidt@mpi-sb.mpg.de

May 9, 1997

Propositional modal logics are increasingly being used in various fields of computer science. Many propositional modal logics are decidable, but a serious problem in real applications is the lack of sophisticated modal theorem provers. Some theorem provers are available that are based on Gentzen or tableaux calculi, of which none have the level of sophistication that first-order theorem provers like otter or spass [5] have. However, unrestricted resolution is merely a semi-decision procedure, so an important and non-trivial problem is finding suitable translation methods and resolution calculi that render decision procedures for modal logics. The standard semantics based translation approach of modal formulae, and entire logics, is based on the possible worlds semantics. It transforms modal formulae to restricted quantifier expressions involving binary relations. The problem with this relational translation approach is the inherent non-determinism in relations, manifested in the non-termination of standard resolution procedures (and complications in other theorem proving approaches). The alternative translation approaches due to [2] and others, that are based on a functional alternative view of the semantics of modal logic, solve the problem of non-determinism. In the functional semantics accessibility is defined by sets of functions replacing binary relations. This reformulation has computational advantages that I will speak about. My talk will be devoted to decidability by the resolution method and an empirical performance analysis that shows our methods can be used in practise.

I exhibit what has often been claimed for the resolution method but never substantiated: For many propositional modal logics unrestricted resolution decides modal satisfiability and theoremhood [4]. Important for decidability is that we use an optimised version of the functional translation approach [3]. It eliminates in the clausal forms all Skolem functions other than Skolem constants, and embeds modal logics in a hierarchy of clausal logics, called path logics. The basic path logic is associated with the basic modal logics K and K_{(m)} as well as KD, and is a fragment of monadic first-order logic with function symbols. Basic path logic includes only nullary functions and one designated binary function, namely juxtaposition. Terms are strings of variables and constant, and encode accessibility as paths from the initial world. Paths are linear terms with different occurrences of one variable in any clause having the same prefix.

∗Extended abstract of a talk to be presented at ESSLLI’97, Aix-en-Provence, August 1997.

We prove a general result that unrestricted resolution and condensing is a decision procedure for the satisfiability problem of formulae in certain path logics, including basic path logic. The result is very powerful for a number of reasons. It immediately follows that standard unrestricted resolution is a decision procedure for many non-transitive uni- or multi-modal logics, including K and arbitrary extensions with D, T and B, as well as their multi-modal versions, and also S5. The result provides an alternative decision proof for the relevant modal logics, and related logics used in applications, like description logics in knowledge representation. This alone is not very exciting. A more far-reaching consequence of the result has practical value, namely, any standard first-order theorem prover that is based on resolution can serve as a reasonable and efficient inference tool for doing modal reasoning. It is not our intention to pursue the use of unrestricted resolution, but the decision result gives us complete freedom to fine tune our theorem prover with any modifications and refinements that are compatible with resolution so as to increase efficiency. We have encouraging benchmark results with the theorem prover spass using ordering refinements [1] that I will present.

References

[1] U. Hustadt and R. A. Schmidt. On evaluating decision procedures for modal logics. In Proc. IJCAI’97, August 1997. To appear. The long version is available as Research Report MPI-I-97-2-003, Max-Planck-Institut für Informatik, Saarbrücken, Germany.

[2] H. J. Ohlbach. Semantics based translation methods for modal logics. Journal of Logic and Computation, 1(5):691–746, 1991.

[3] H. J. Ohlbach and R. A. Schmidt. Functional translation and second-order frame properties of modal logics. Technical Report MPI-I-95-2-002, Max-Planck-Institut für Informatik, Saarbrücken, Germany, January 1995. To appear in Journal of Logic and Computation.

[4] R. A. Schmidt. Resolution is a decision procedure for many propositional modal logics: Extended abstract. To appear in Kracht, M., de Rijke, M., Wansing, H. and Zakharyaschev, M. (eds) (1997), Advances in Modal Logic ‘96, CSLI Publications., 1997.

[5] C. Weidenbach, B. Gaede, and G. Rock. spass & flotter, version 0.42. In M. A. McRobbie and J. K. Slaney, editors, Automated Deduction: CADE-13, volume 1104 of Lecture Notes in Artificial Intelligence, pages 141–145. Springer, 1996.