A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments

Schmidt, R. A. and Tishkovsky, D. (2008)

In Armando, A., Baumgartner, P. and Dowek, G. (eds), Automated Reasoning (IJCAR 2008). Lecture Notes in Computer Science, Vol. 5195, Springer, 194-209. BiBTeX, DOI Link.

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.

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

Last modified: 01 Sep 08
Copyright © 2008 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk