A Resolution-Based Decision Procedure for Extensions of K4

Ganzinger, H., Hustadt, U., Meyer, C. and Schmidt, R. A. (2001)

In Zakharyaschev, M. and Segerberg, K. and de Rijke, M. and Wansing, H. (eds), Advances in Modal Logic, Volume 2. Lecture Notes 119, CSLI Publications, Stanford, 225-246. BiBTeX, PostScript.

This paper presents a resolution decision procedure for transitive propositional modal logics. The procedure combines the relational translation method with an ordered chaining calculus designed to avoid unnecessary inferences with transitive relations. We show the logics K4, KD4 and S4 can be transformed into a bounded class of well-structured clauses closed under ordered resolution and negative chaining.

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 27 Apr 2001
Copyright © 1999-2001 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk