@INPROCEEDINGS{SchmidtTishkovsky08b,
AUTHOR = {Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2008},
TITLE = {A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments},
EDITOR = {Armando, A. and Baumgartner, P. and Dowek, G.},
BOOKTITLE = {Automated Reasoning (IJCAR 2008)},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {5195},
PUBLISHER = {Springer},
PAGES = {194--209},
ISBN = {978-3-540-71069-1},
DOI = {http://dx.doi.org/10.1007/978-3-540-71070-7_17},
URL = {http://www.springerlink.com/content/a2020123406331w5/fulltext.pdf},
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, as well as 
description logics such as ALC 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.
}
}