David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
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)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Rajeev 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. [REVIEW] 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):437-464.
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.
Added to index2009-01-28
Total downloads8 ( #192,398 of 1,410,185 )
Recent downloads (6 months)1 ( #177,870 of 1,410,185 )
How can I increase my downloads?