A general tableau method for deciding description logics, modal logics and related first-order fragments

Abstract

This paper presents a general method for proving termination of tableaux-based procedures for modal-type logics and related first-order fragments. The method is based on connections between filtration arguments and tableau blocking techniques. The method provides a general framework for developing tableau-based decision procedures for a large class of logics. In particular, the method can be applied to many well-known description and modal logics. The class includes traditional modal logics such as S4 and modal logics with the universal modality, ALC as well as description logics such as with nominals and general TBoxes. Also contained in the class are harder and less well-studied modal logics with complex modalities and description logics with complex role operators such as Boolean modal logic, and the description logic ALBO. In addition, the techniques allow us to specify tableau-based decision procedures for related solvable fragments of first-order logic, including the two-variable fragment of first-order logic. © 2008 Springer-Verlag Berlin Heidelberg.