H. de Nivelle, R. A. Schmidt, and U. Hustadt(2000): ``Resolution-Based Methods for Modal Logics.'' Logic Journal of the IGPL (8)3:265-292.
Abstract, BibTeX, Abstract + PDF (Oxford University Press), Errata.

In this paper we give an overview of a selection of proof systems for propositional modal logics, namely, standard tableaux, modal KE tableaux, modal resolution and translation-based resolution. We will concentrate on translation-based resolution methods describing different translation-methods and various refinements of resolution. We also discuss how tableaux and modal resolution methods can be simulated in the general framework of resolution. [an error occurred while processing this directive]