Studia Logica 72 (2):199-232 (2002)
The aim of this paper is to construct a tableau decision algorithm for the modal description logic K ALC with constant domains. More precisely, we present a tableau procedure that is capable of deciding, given an ALC-formula with extra modal operators (which are applied only to concepts and TBox axioms, but not to roles), whether is satisfiable in a model with constant domains and arbitrary accessibility relations. Tableau-based algorithms have been shown to be practical even for logics of rather high complexity. This gives us grounds to believe that, although the satisfiability problem for K ALC is known to be NEXPTIME-complete, by providing a tableau decision algorithm we demonstrate that highly expressive description logics with modal operators have a chance to be implementable. The paper gives a solution to an open problem of Baader and Laux .
|Keywords||Philosophy Logic Mathematical Logic and Foundations Computational Linguistics|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Cut-Free Sequent and Tableau Systems for Propositional Diodorean Modal Logics.Rajeev Goré - 1994 - Studia Logica 53 (3):433 - 457.
ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse.Linh Anh Nguyen & Andrzej Szałas - 2011 - Studia Logica 98 (3):387-428.
Temporalising Tableaux.Roman Kontchakov, Carsten Lutz, Frank Wolter & Michael Zakharyaschev - 2004 - Studia Logica 76 (1):91 - 134.
A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics.Rajeev Gore - unknown
A Sound and Complete Tableau Calculus for Reasoning About Only Knowing and Knowing at Most.Riccardo Rosati - 2001 - Studia Logica 69 (1):171-191.
Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD.Linh Anh Nguyen - 2001 - Studia Logica 69 (1):41-57.
Terminating Tableau Systems for Hybrid Logic with Difference and Converse.Mark Kaminski & Gert Smolka - 2009 - Journal of Logic, Language and Information 18 (4):437-464.
Theory Matrices (for Modal Logics) Using Alphabetical Monotonicity.Ian P. Gent - 1993 - Studia Logica 52 (2):233 - 257.
A Tableau Method for Graded Intersections of Modalities: A Case for Concept Languages. [REVIEW]Ani Nenkova - 2002 - Journal of Logic, Language and Information 11 (1):67-77.
An Overview of Tableau Algorithms for Description Logics.Franz Baader & Ulrike Sattler - 2001 - Studia Logica 69 (1):5-40.
Added to index2009-01-28
Total downloads29 ( #177,582 of 2,171,776 )
Recent downloads (6 months)1 ( #326,702 of 2,171,776 )
How can I increase my downloads?