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 develo** 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 \(\mathcal{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 \(\mathcal{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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abate, P., Goré, R.: The Tableaux Work Bench. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol. 2796, pp. 230–236. Springer, Heidelberg (2003)
Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Stud. Log. 69, 5–40 (2001)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Camb. Tracts Theor. Comput. Sci, vol. 53. Cambridge University Press, Cambridge (2001)
Castilho, M.A., Fariñas del Cerro, L., Gasquet, O., Herzig, A.: Modal tableaux with propagation rules and structural rules. Fundam. Inform. 3-4(32), 281–297 (1997)
Fariñas del Cerro, L., Gasquet, O., Herzig, A., Sahade, M.: Modal tableaux: Completeness vs. termination. In: We Will Show Them!, vol. 1, pp. 587–614. College Publ. (2005)
Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-Dimensional Modal Logics: Theory and Applications. North-Holland, Amsterdam (2003)
Gabbay, D.M., Shehtman, V.: Products of modal logics, part 1. Log. J. IGPL 6(1), 73–146 (1998)
Gargov, G., Passy, S., Tinchev, T.: Modal environment for Boolean speculations. In: Proc. Gödel 1986, Plenum, pp. 253–263 (1987)
Gasquet, O., Herzig, A., Sahade, M.: Terminating modal tableaux with simple completeness proof. In: Proc. AiML 2006, pp. 167–186. College Publ. (2006)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Heuerding, A., Jäger, G., Schwendimann, S., Seyfried, M.: The Logics Workbench LWB: A snapshot. Euromath. Bull. 2(1), 177–186 (1996)
Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput. 9(3), 385–410 (1999)
Schmidt, R.A., Tishkovsky, D.: A general tableau method for deciding description logics, modal logics and related first-order fragments, http://www.cs.man.ac.uk/~dmitry/papers/gtm2008.pdf
Schmidt, R.A., Tishkovsky, D.: Using tableau to decide expressive description logics with role negation. In: Aberer, K., Choi, K.-S., Noy, N., Allemang, D., Lee, K.-I., Nixon, L., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudré-Mauroux, P. (eds.) ISWC 2007. LNCS, vol. 4825, pp. 438–451. Springer, Heidelberg (2007)
Tishkovsky, D.: MetTel system, http://www.cs.man.ac.uk/dmitry/implementations/MetTeL/
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt, R.A., Tishkovsky, D. (2008). A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. In: Armando, A., Baumgartner, P., Dowek, G. (eds) Automated Reasoning. IJCAR 2008. Lecture Notes in Computer Science(), vol 5195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71070-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-71070-7_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71069-1
Online ISBN: 978-3-540-71070-7
eBook Packages: Computer ScienceComputer Science (R0)