Non-standard reasoning in Description Logics (DLs) comprises computing a Least Common Subsumer (LCS), a Concept Difference, a Concept Unifier, or an Interpolant Concept, to name a few. Although some reasoning services have been unified already (e.g., LCS andMost Specific Concept), the definition of non-standard problems and the computation that solve them are very different from each other. We propose to unify the definitions of non-standard services as special Second-order sentences in DLs; when the solution concepts are optimal with respect to some preferences, a fixpoint replaces the Second-order quantification. Moreover, we propose to combine the well-known Tableaux calculi for DLs with rules that compute substitutions of Concept Variables. We prove soundness and completeness of the combined calculus and we give a sufficient condition for termination, which covers some non-trivial cases.
|Titolo:||A Unified Framework for Non-standard Reasoning Services in Description Logics|
|Data di pubblicazione:||2010|
|Nome del convegno:||19th European Conference on Artificial Intelligence, ECAI 2010|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.3233/978-1-60750-606-5-479|
|Appare nelle tipologie:||4.1 Contributo in Atti di convegno|