A tableau decision algorithm for modalized ALC with constant domains
Studia Logica 72 (2):199-232 (2002)
| Abstract | 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 [5]. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,705 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesRajeev Goré (1994). Cut-Free Sequent and Tableau Systems for Propositional Diodorean Modal Logics. Studia Logica 53 (3):433 - 457.
Ani Nenkova (2002). A Tableau Method for Graded Intersections of Modalities: A Case for Concept Languages. Journal of Logic, Language and Information 11 (1):67-77.
Ian P. Gent (1993). Theory Matrices (for Modal Logics) Using Alphabetical Monotonicity. Studia Logica 52 (2):233 - 257.
Mark Kaminski & Gert Smolka (2009). Terminating Tableau Systems for Hybrid Logic with Difference and Converse. Journal of Logic, Language and Information 18 (4).
Linh Anh Nguyen (2001). Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD. Studia Logica 69 (1):41-57.
Riccardo Rosati (2001). A Sound and Complete Tableau Calculus for Reasoning About Only Knowing and Knowing at Most. Studia Logica 69 (1):171-191.
Roman Kontchakov, Carsten Lutz, Frank Wolter & Michael Zakharyaschev (2004). Temporalising Tableaux. Studia Logica 76 (1):91 - 134.
Linh Anh Nguyen & Andrzej Szałas (2011). ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse. Studia Logica 98 (3):387-428.
Franz Baader & Ulrike Sattler (2001). An Overview of Tableau Algorithms for Description Logics. Studia Logica 69 (1):5-40.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2009-01-28Total downloads0Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
