Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Publications
2008
Franz Baader, Sebastian Brandt, and Carsten Lutz.
Pushing the EL Envelope Further.
In Kendall Clark and Peter F. Patel-Schneider, editors, In Proceedings of
the OWLED 2008 DC Workshop on OWL: Experiences and Directions, 2008.
Bibtex entry Paper (PDF)
Abstract
We extend the description logic EL++ with reflexive roles and range
restrictions, and show that subsumption remains tractable if a certain
syntactic restriction is adopted. We also show that subsumption
becomes PSpace-hard (resp. undecidable) if this restriction is
weakened (resp. dropped). Additionally, we prove that tractability is
lost when symmetric roles are added: in this case, subsumption becomes
ExpTime- hard.
Franz Baader and Felix Distel.
A Finite Basis for the Set of EL-Implications Holding in a Finite
Model.
In Raoul Medina and Sergei Obiedkov, editors, Proceedings of the 6th
International Conference on Formal Concept Analysis, (ICFCA 2008), volume
4933 of Lecture Notes in Artificial Intelligence, pages 46–61.
Springer, 2008.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag
Abstract
Formal Concept Analysis (FCA) can be used to analyze data given in the form of a formal context. In particular, FCA provides efficient algorithms for computing a minimal basis of the implications holding in the context. In this paper, we extend classical FCA by considering data that are represented by relational structures rather than formal contexts, and by replacing atomic attributes by complex formulae defined in some logic. After generalizing some of the FCA theory to this more general form of contexts, we instantiate the general framework with attributes defined in the Description Logic (DL) EL, and with relational structures over a signature of unary and binary predicates, i.e., models for EL. In this setting, an implication corresponds to a so-called general concept inclusion axiom (GCI) in EL, The main technical result of this paper is that, in EL, for any finite model there is a \emph{finite} set of implications (GCIs) holding in this model from which all implications (GCIs) holding in the model follow.
Franz Baader, Silvio Ghilardi, and Carsten Lutz.
LTL over Description Logic Axioms.
In Proceedings of the 21st International Workshop on Description Lo gics
(DL2008), volume 353 of CEUR-WS, 2008.
Bibtex entry Paper
(PDF)
Abstract
Most of the research on temporalized Description Logics (DLs) has
concentrated on the most general case where temporal operators can
occur both within DL concepts and in front of DL axioms. In this
setting, reasoning usually becomes quite hard. If rigid roles (i.e.,
roles whose interpretation does not vary over time) are allowed, then
the interesting inference problems (such as satisfiability of
concepts) become undecidable. Even if all symbols are interpreted as
flexible (i.e., their interpretations can change arbitrarily from one
time-point to the next), the complexity of reasoning is doubly
exponential, i.e., one exponential higher than the complexity of
reasoning in pure DLs such as ALC. In this paper, we consider the case
where temporal operators are allowed to occur only in front of axioms
(i.e., ABox assertions and general concept inclusion axioms (GCIs)),
but not inside concepts. As the temporal component, we use linear
temporal logic (LTL) and in the DL component we consider ALC. We show
that reasoning becomes simpler in this setting.
Franz Baader, Silvio Ghilardi, and Carsten Lutz.
LTL over Description Logic Axioms.
In Proceedings of the 11th International Conference on Principles of
Knowledge Representation and Reasoning (KR2008), 2008.
Bibtex entry Paper (PDF)
Abstract
Most of the research on temporalized Description Logics (DLs) has
concentrated on the case where temporal operators can occur within DL
concept descriptions. In this setting, reasoning usually becomes
quite hard if rigid roles, i.e., roles whose interpretation does not
change over time, are available. In this paper, we consider the case
where temporal operators are allowed to occur only in front of DL
axioms (i.e., ABox assertions and general concept inclusion axioms),
but not inside of concepts descriptions. As the temporal component,
we use linear temporal logic (LTL) and in the DL component we consider
the basic DL ALC. We show that reasoning in the presence of rigid
roles becomes considerably simpler in this setting.
Franz Baader, Jan Hladik, and Rafael Peñaloza.
Automata Can Show PSPACE Results for Description Logics.
Information and Computation, Special Issue: First International Conference
on Language and Automata Theory and Applications (LATA'07),
206(9–10):1045–1056, 2008.
Bibtex entry Paper (PDF)
Abstract
In the area of Description Logic (DL), both tableau-based and automata-based
algorithms are frequently used to show decidability and complexity results
for basic inference problems such as satisfiability of concepts. Whereas
tableau-based algorithms usually yield worst-case optimal algorithms in the
case of PSPACE-complete logics, it is often very hard to design optimal
tableau-based algorithms for EXPTIME-complete DLs. In contrast, the
automata-based approach is usually well-suited to prove EXPTIME
upper-bounds, but its direct application will usually also yield an
EXPTIME-algorithm for a PSPACE-complete logic since the (tree) automaton
constructed for a given concept is usually exponentially large. In the
present paper, we formulate conditions under which an on-the-fly
construction of such an exponentially large automaton can be used to obtain
a PSPACE-algorithm. We illustrate the usefulness of this approach by
proving a new PSPACE upper-bound for satisfiability of concepts with
respect to acyclic terminologies in the DL SI, which extends the basic DL
ALC with transitive and inverse roles.
Franz Baader, Novak Novakovic, and Boontawee Suntisrivaraporn.
A Proof-Theoretic Subsumption Reasoner for Hybrid
EL-TBoxes.
In Proceedings of the 2008 International Workshop on Description Logics
(DL2008), volume 353 of CEUR-WS, 2008.
Bibtex entry Paper (PDF)
Abstract
Hybrid EL-TBoxes combine general concept inclusions (GCIs), which are interpreted with descriptive semantics, with cyclic concept definitions, which are interpreted with greatest fixpoint (gfp) semantics. We introduce a proof-theoretic approach that yields a polynomial-time decision procedure for subsumption in EL w.r.t. hybrid TBoxes, and present preliminary experimental results regarding the performance of the reasoner Hyb that implements this decision procedure.
Franz Baader and Rafael Peñaloza.
Automata-Based Axiom Pinpointing.
In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors,
Proceedings of the 4th International Joint Conference on Automated Reasoning,
(IJCAR 2008), volume 5195 of Lecture Notes in Artificial
Intelligence, pages 226–241. Springer, 2008.
Bibtex entry Paper
(PDF) ©Springer-Verlag
Abstract
Axiom pinpointing has been introduced in description logics (DL) to help the user understand
the reasons why consequences hold by computing minimal subsets of the knowledge base that
have the consequence in question (MinA). Most of the pinpointing algorithms described in the
DL literature are obtained as extensions of tableau-based reasoning algorithms for computing
consequences from DL knowledge bases. In this paper, we show that automata-based algorithms
for reasoning in DLs can also be extended to pinpointing algorithms. The idea is that the
tree automaton constructed by the automata-based approach can be transformed into a weighted
tree automaton whose so-called behaviour yields a pinpointing formula, i.e., a monotone
Boolean formula whose minimal valuations correspond to the MinAs. We also develop an approach
for computing the bahaviour of a given weighted tree automaton.
Franz Baader and Boontawee Suntisrivaraporn.
Debugging SNOMED CT Using Axiom Pinpointing in the Description Logic
EL^+.
In Proceedings of the 3rd Knowledge Representation in Medicine (KR-MED'08):
Representing and Sharing Knowledge Using SNOMED, volume 410 of
CEUR-WS, 2008.
Bibtex entry Paper (PDF)
Abstract
SNOMED CT is a large-scale medical ontology, which is developed using a variant of the inexpressive Description Logic EL. Description Logic reasoning can not only be used to compute subsumption relationships between SNOMED concepts, but also to pinpoint the reason why a certain subsumption relationship holds by computing the axioms responsible for this relationship. This helps developers and users of SNOMED CT to understand why a given subsumption relationship follows from the ontology, which can be seen as a first step toward removing unwanted subsumption relationships.
In this paper, we describe a new method for axiom pinpointing in the Description Logic EL+, which is based on the computation so-called reachability-based modules. Our experiments on SNOMED CT show that the sets of axioms explaining subsumption are usually quite small, and that our method is fast enough to compute such sets on demand.
Meghyn Bienvenu.
Complexity of Abduction in the EL Family of Lightweight Description
Logics.
In Gerhard Brewka and Jérôme Lang, editors, Proceedings of the
Eleventh International Conference on Principles of Knowledge Representation
and Reasoning (KR08), pages 220–230. AAAI Press, 2008.
Bibtex entry Paper
(PDF)
Abstract
The complexity of logic-based abduction has been extensively studied for the case in which the background knowledge is represented by a propositional theory, but very little is known about abduction with respect to description logic knowledge bases. The purpose of the current paper is to examine the complexity of logic-based abduction for the EL family of lightweight description logics. We consider several minimality criteria for explanations (set inclusion, cardinality, prioritization, and weight) and three decision problems: deciding whether an explanation exists, deciding whether a given hypothesis appears in some acceptable explanation, and deciding whether a given hypothesis belongs to every acceptable explanation. We determine the complexity of these tasks for general TBoxes and also for EL and EL+ terminologies. We also provide results concerning the complexity of computing abductive explanations.
Meghyn Bienvenu.
Prime Implicate Normal Form for ALC Concepts.
In Proceedings of the Twenty-Third Conference on Artificial Intelligence
(AAAI-08), pages 412–417. AAAI Press, 2008.
Bibtex entry Paper (PDF)
Abstract
In this paper, we present a normal form for concept expressions in the description logic ALC which is based on a recently introduced notion of prime implicate for the modal logic K. We show that concepts in prime implicate normal form enjoy a number of interesting properties. In particular, we prove that subsumption between ALC concepts in prime implicate normal form can be carried out in polynomial time using a simple structural subsumption algorithm reminiscent of those used for less expressive description logics. We provide a sound and complete algorithm for putting concepts into prime implicate normal form, and we investigate the spatial complexity of this transformation, showing there to be an at most doubly-exponential blowup in concept length. At the end of the paper, we compare prime implicate normal form to two other normal forms for ALC, discussing the relative merits of the different approaches.
Birte Glimm, Carsten Lutz, Ian Horrocks, and Ulrike Sattler.
Answering conjunctive queries in the SHIQ description
logic.
Journal of Artificial Intelligence Research, 31:150–197, 2008.
Bibtex entry Paper (PDF)
Abstract
Conjunctive queries play an important role as an expressive query
language for Description Logics (DLs). Although modern DLs usually
provide for transitive roles, conjunctive query answering over DL
knowledge bases is only poorly understood if transitive roles are
admitted in the query. In this paper, we consider unions of
conjunctive queries over knowledge bases formulated in the prominent
DL SHIQ and allow transitive roles in both the query and the knowledge
base. We show decidability of query answering in this setting and
establish two tight complexity bounds: regarding combined complexity,
we prove that there is a deterministic algorithm for query answering
that needs time single exponential in the size of the KB and double
exponential in the size of the query, which is optimal. Regarding data
complexity, we prove containment in co-NP.
Christoph Haase and Carsten Lutz.
Complexity of Subsumption in the EL Family of Description Logics: Acyclic
and Cyclic TBoxes.
In Malik Ghallab, Constantine D. Spyropoulos, Nikos Fakotakis, and Nikos
Avouris, editors, Proceedings of the 18th European Conference on
Artificial Intelligence (ECAI08), volume 178 of Frontiers in
Artificial Intelligence and Applications, pages 25–29. IOS Press, 2008.
Bibtex entry Paper (PDF)
Abstract
We perform an exhaustive study of the complexity of subsumption in
the EL family of lightweight description logics w.r.t. acyclic and
cyclic TBoxes. It turns out that there are interesting members of
this family for which subsumption w.r.t. cyclic TBoxes is
tractable, whereas it is ExpTime-complete w.r.t. general TBoxes.
For other extensions that are intractable w.r.t. general TBoxes, we
establish intractability already for acyclic and cyclic TBoxes.
Matthias Heinrich, Antje Boehm-Peters, and Martin Knechtel.
MoDDo - a tailored documentation system for model-driven software
development.
In ICWI '08: Proceedings of the IADIS International Conference
WWW/Internet, pages 321–324, 2008.
Bibtex entry Paper
(PDF)
Abstract
In the last decade Model-Driven Software Development (MDSD) has become an established software engineering
discipline. The new approach dramatically changed the entire software development lifecycle. However, the
documentation process was not adapted and stuck with the old paradigms. In this paper, we propose a model-driven
documentation system which is adapted to the MDSD lifecycle and therefore exploits synergies coming along with the
alignment of software development and software documentation. Furthermore, the proposed documentation system builds
upon the Internet as their major provisioning platform.
Miki Hermann and Baris Sertkaya.
On the Complexity of Computing Generators of Closed Sets.
In Raoul Medina and Sergei A. Obiedkov, editors, Proceedings of the 6th
International Conference on Formal Concept Analysis, (ICFCA
2008), volume 4933 of Lecture Notes in Computer Science, pages
158–168. Springer Verlag, 2008.
Bibtex
entry Paper
(PDF) ©Springer-Verlag
Abstract
We investigate the computational complexity of some decision and
counting problems related to generators of closed sets fundamental
in Formal Concept Analysis. We recall results from the literature
about the problem of checking the existence of a generator with a
specified cardinality, and about the problem of determining the
number of minimal generators. Moreover, we show that the problem of
counting minimum cardinality generators is #.coNP-complete. We
also present an incremental-polynomial time algorithm from
relational database theory that can be used for computing all
minimal generators of an implication-closed set.
Martin Knechtel.
Access restriction inside ontologies.
In Rainer Ruggaber, editor, I-ESA'08: Proceedings of the 1st Internet of
Services Doctoral Symposium 2008 at International Conference on
Interoperability of Enterprise Systems and Applications, volume 374 of
CEUR Workshop Proceedings, ISSN 1613-0073, Berlin, Germany, 2008.
Bibtex entry Paper (PDF)
Martin Knechtel.
Access rights and collaborative ontology integration for reuse across
security domains.
In Philippe Cudré-Mauroux, editor, Proceedings of the ESWC 2008 Ph.D.
Symposium, volume 358 of CEUR Workshop Proceedings, ISSN
1613-0073, pages 36–40, 2008.
Bibtex entry Paper (PDF)
Martin Knechtel and Jan Hladik.
RBAC Authorization Decision with DL Reasoning.
In ICWI '08: Proceedings of the IADIS International Conference
WWW/Internet, pages 169–176, 2008.
Bibtex entry Paper
(PDF)
Abstract
Access control is crucial also for the Semantic Web. Technologies and Standards from the Semantic Web Community
itself provide powerful means to model access control definitions and automatically reason about them. We extend
Hierarchical Role Based Access Control by a class hierarchy of the accessed objects and give it the name RBAC-CH. We
present a concept to implement this model in a DL knowledge base in the form of an OWL 1.1 ontology. The permissions
are defined for user roles on object classes. The concrete permissions of users to objects are then automatically derived by
a reasoning service. We present a straightforward ontology model and evaluate it in a running example with a state of the
art reasoner. For the RBAC policy enforcement we need to run the reasoner only once and at runtime we only need to
read out the inferred knowledge base to decide about authorization.
Martin Knechtel, Jan Hladik, and Frithjof Dau.
Using OWL DL Reasoning to decide about authorization in RBAC.
In Catherine Dolbear, Alan Ruttenberg, and Ulrike Sattler, editors, OWLED
'08: Proceedings of the OWLED 2008 Workshop on OWL: Experiences and
Directions, volume 432 of CEUR Workshop Proceedings, 2008.
Bibtex entry Paper (PDF)
Martin Knechtel and Daniel Schuster.
Semantische Integration und Wiederverwendung von Produktontologien
für offene Marktplätze im Web.
In Proceedings of GeNeMe'08 Workshop, 2008.
In German.
Bibtex entry Paper (PDF)
Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolte r.
Logical Difference and Module Extraction with CEX and MEX.
In Proceedings of the 21st International Workshop on Description Lo gics
(DL2008), volume 353 of CEUR-WS, 2008.
Bibtex entry Paper (PDF)
Abstract
In this paper, we study the module extraction and logical difference
problems for acyclic EL-terminologies. We show that both problems are
tractable, present prototype implementations, and evaluate performance
on a series of examples. In particular, our implementations can handle
large real-world terminologies such as SNOMED-CT.
Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter.
CEX and MEX: Logical Diff and Semantic Module Extraction in a Fragment of
OWL.
In Kendall Clark and Peter F. Patel-Schneider, editors, In Proceedings of
the OWLED 2008 DC Workshop on OWL: Experiences and Directions, 2008.
Bibtex entry Paper (PDF)
Abstract
We consider a logical diff operator and semantic module extraction
from ontologies. In recent work, we have shown that, for the fragment
EL of OWL, these problems can be solved in polynomial time. In this
paper, we evaluate our algorithms by experimenting with the prototype
implementations CEX and MEX on real-worlds ontologies such as
SNOMED. The experiments show the practicability our approach and
highlight the benefits of a strictly semantic approach: the diff
operation is very fine-grained and the extracted modules are smaller
than the ones generated by related approaches.
Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter.
Formal Properties of Modularisation.
In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors,
Proceedings of the 4th International Joint Conference on Automated Reasoning
(IJCAR2008), number 5195 in LNCS, pages 179–193. Springer, 2008.
Bibtex entry Paper (PDF)
Abstract
Modularity of ontologies is currently an active research field, and
many different notions of a module have been proposed. In this
paper, we review the fundamental principles of modularity and
identify formal properties that a robust notion of modularity should
satisfy. We explore these properties in detail in the contexts of
description logic and classical predicate logic and put them into
the perspective of well-known concepts from logic and modular
software specification such as interpolation, forgetting and
uniform interpolation. We also discuss reasoning problems related to
modularity.
Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter.
Semantic Modularity and Module Extraction in Description Logics.
In Malik Ghallab, Constantine D. Spyropoulos, Nikos Fakotakis, and Nikos
Avouris, editors, Proceedings of the 18th European Conference on
Artificial Intelligence (ECAI08), volume 178 of Frontiers in
Artificial Intelligence and Applications, pages 55–59. IOS Press, 2008.
Bibtex entry Paper (PDF)
Abstract
The aim of this paper is to study semantic notions of modularity in
description logic (DL) terminologies and reasoning problems that are
relevant for modularity. We define two notions of a module whose
independence is formalized in a model-theoretic way. Focusing mainly
on the DLs EL and ALC, we the develop algorithms for module
extraction, for checking whether a part of a terminology is a module,
and for a number of related problems. We also analyse the complexity
of these problems, which ranges from tractable to
undecidable. Finally, we provide an experimental evaluation of our
module extraction algorithms based on the large-scale terminology
SNOMED CT.
Hongkai Liu, Carsten Lutz, and Maja Milicic.
The Projection Problem for EL Actions.
In Proceedings of the 2008 International Workshop on Description Logics
(DL2008), volume 353 of CEUR-WS, 2008.
Bibtex entry Paper
(PDF)
Abstract
In this paper, we investigate the complexity of executability and
projection in EL and the extension of EL with atomic
negation. In both cases, we allow for negated assertions in the
post-conditions of actions. Our results show that, in general,
tractability does not transfer from instance checking in EL to executability
and projection. Even in EL without TBoxes, the latter problems are
co-NP-hard. This is due to two sources of intractability:
(1) existential restrictions in the initial ABox together with negated
assertions in post-conditions; and (2) conditional post-conditions.
We prove a matching co-NP upper bound for EL with atomic negation. We also
show that, in the presence of acyclic TBoxes, projection in EL is
PSpace-hard and thus not easier than in ALC. Finally, we identify
restrictions under which executability and projection in EL w.r.t.
acyclic TBoxes can be decided in polynomial time.
Carsten Lutz.
The Complexity of Conjunctive Query Answering in Expressive Description
Logics.
In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors,
Proceedings of the 4th International Joint Conference on Automated Reasoning
(IJCAR2008), number 5195 in LNAI, pages 179–193. Springer, 2008.
Bibtex
entry Paper
(PDF)
Abstract
Conjunctive query answering plays a prominent role in applications
of description logics (DLs) that involve instance data, but its
exact complexity was a long-standing open problem. We determine the
complexity of conjunctive query answering in expressive DLs between
ALC and SHIQ, and thus settle the problem. In a nutshell, we show
that conjunctive query answering is 2ExpTime-complete in the
presence of inverse roles, and only ExpTime-complete without them.
Carsten Lutz.
Two Upper Bounds for Conjunctive Query Answering in SHIQ.
In Proceedings of the 21st International Workshop on Description Logics
(DL2008), volume 353 of CEUR-WS, 2008.
Bibtex
entry Paper
(PDF)
Abstract
We have shown recently that, in extensions of ALC that involve
inverse roles, conjunctive query answering is harder than
satisfiability: it is 2-ExpTime-complete in general and
NExpTime-hard if queries are connected and contain at least one
answer variable. In this paper, we show that, in
SHIQ without inverse roles (and without transitive roles in the
query), conjunctive query answering is only ExpTime-complete and
thus not harder than satisfiability. We also show that the
mentioned NExpTime-lower bound is tight.
Carsten Lutz, Frank Wolter, and Michael Zakharyaschev.
Temporal Description Logics: A Survey.
In Proceedings of the Fifteenth International Symposium on Temporal
Representation and Reasoning. IEEE Computer Society Press, 2008.
Bibtex entry Paper (PDF)
Abstract
We survey temporal description logics that are based on standard
temporal logics such as LTL and CTL. In particular, we concentrate
on the computational complexity of the satisfiability problem and
algorithms for deciding it.
Rafael Peñaloza.
Automata-based Pinpointing for DLs.
In Proceedings of the 2008 International Workshop on Description Logics
(DL2008), volume 353 of CEUR-WS, 2008.
Bibtex
entry Paper
(PDF)
Abstract
The task of pinpointing the relevant subsets of axioms for a given property has acquired relevancy in the last years. In this paper we show how automata-based decision procedures can be adapted to produce a so-called pinpointing formula. The relevance of this method is method is shown by giving an (optimal) algorithm that computes pinpointing formulas for unsatisfiability of SI concepts w.r.t. general TBoxes.
Stefan Schulz, Kornél Markó, and Boontawee Suntisrivaraporn.
Formal representation of complex SNOMED CT expressions.
BMC Medical Informatics and Decision Making, 8(1):S9, 2008.
Bibtex entry Paper (PDF)
Abstract
Background:
Definitory expressions about clinical procedures, findings and diseases constitute a major benefit of a formally founded clinical reference terminology which is ontologically sound and suited for formal reasoning. SNOMED CT claims to support formal reasoning by description-logic based concept definitions.
Methods:
On the basis of formal ontology criteria we analyze complex SNOMED CT concepts, such as "Concussion of Brain with(out) Loss of Consciousness", using alternatively full first order logics and the description logic EL.
Results:
Typical complex SNOMED CT concepts, including negations or not, can be expressed in full first-order logics. Negations cannot be properly expressed in the description logic EL underlying SNOMED CT. All concepts concepts the meaning of which implies a temporal scope may be subject to diverging interpretations, which are often unclear in SNOMED CT as their contextual determinants are not made explicit.
Conclusion:
The description of complex medical occurrents is ambiguous, as the same situations can be described as (i) a complex occurrent C that has A and B as temporal parts, (ii) a simple occurrent A' defined as a kind of A followed by some B, or (iii) a simple occurrent B' defined as a kind of B preceded by some A. As negative statements in SNOMED CT cannot be exactly represented without a (computationally costly) extension of the set of logical constructors, a solution can be the reification of negative statments (e.g., "Period with no Loss of Consciousness"), or the use of the SNOMED CT context model. However, the interpretation of SNOMED CT context model concepts as description logics axioms is not recommended, because this may entail unintended models.
Baris Sertkaya.
Explaining User Errors in Description Logic Knowledge Base Completion.
In Informal Proceedings of the 2008 International Workshop on Complexity,
Expressibility, and Decidability in Automated Reasoning (CEDAR'08),
2008.
Bibtex
entry Paper
(PDF)
Abstract
In our previous work we have developed a method for
completing a Description Logic knowledge base w.r.t. a fixed interpretation
by asking questions to a domain expert.
Our experiments showed that during this process the domain expert sometimes
gives wrong answers to the questions, which cause the resultant knowledge base
to have unwanted consequences. In the present work we consider the problem of
explaining the reasons of such unwanted consequences in knowledge base
completion. We show that in this setting the problem of deciding the existence
of an explanation
within a specified cardinality bound is NP-complete, and the problem of
counting explanations that are minimal w.r.t. set inclusion is #P-complete.
We also provide an algorithm that computes one minimal explanation by
performing at most polynomially many subsumption tests.
Baris Sertkaya.
Explaining User Errors in Knowledge Base Completion.
In Proceedings of the 2008 International Workshop on Description Logics
(DL2008), volume 353 of CEUR-WS, 2008.
Bibtex
entry Paper
(PDF)
Abstract
Knowledge base completion is a method for
extending both the terminological and assertional part of a Description
Logic knowledge base by using information provided by a domain expert.
It ensures that the extended knowledge base is complete w.r.t. a fixed
interpretation in a certain, well-defined sense. Here we consider the
problem of explaining user errors in knowledge base completion. We show
that for this setting, the
problem of deciding the existence of an explanation within a specified
cardinality bound is NP-complete, and the problem of counting
explanations that are minimal w.r.t. set inclusion is #P-complete.
We also provide an algorithm that computes one minimal explanation by
performing at most polynomially many subsumption tests.
Boontawee Suntisrivaraporn.
Empirical evaluation of reasoning in lightweight DLs on life science
ontologies.
In Proceedings of the 2nd Mahasarakham International Workshop on AI
(MIWAI'08), 2008.
Bibtex entry Paper
(PDF)
Abstract
Description Logics (DLs) belong to a successful family of knowledge representation formalisms with two key assets: formally well-dned semantics which allows to represent knowledge in an unambiguous way and automated reasoning which allows to infer implicit knowledge from the one given explicitly. One of the most prominent applications of DLs is their use as ontology languages, especially for the life science domain. This paper investigates several life science ontologies and summarizes their common characteristics. It suggests that the use of lightweight DLs in the EL family, in which reasoning is tractable, is bencial both in terms of expressivity and of scalability. The claim is supported by extensive empirical evaluation of various DL reasoning services on large-scale life science ontologies, including an overview comparison of state-ofthe-art DL reasoners.
Boontawee Suntisrivaraporn.
Module Extraction and Incremental Classification: A Pragmatic Approach for
EL^+ Ontologies.
In Sean Bechhofer, Manfred Hauswirth, Joerg Hoffmann, and Manolis Koubarakis,
editors, Proceedings of the 5th European Semantic Web Conference
(ESWC'08), volume 5021 of Lecture Notes in Computer Science,
pages 230–244. Springer-Verlag, 2008.
Bibtex
entry Paper
(PDF) ©Springer-Verlag
Abstract
The description logic EL+ has recently proved practically useful in the life science domain with presence of several large-scale biomedical ontologies such as SNOMED CT. To deal with ontologies of this scale, standard reasoning of classification is essential but not sufficient. The ability to extract relevant fragments from a large ontology and to incrementally classify it has become more crucial to support ontology design, maintenance and re-use. In this paper, we propose a pragmatic approach to module extraction and incremental classification for EL+ ontologies and report on empirical evaluations of our algorithms which have been implemented as an extension of the CEL reasoner.
Boontawee Suntisrivaraporn, Guilin Qi, Qiu Ji, and Peter Haase.
A Modularization-based Approach to Finding All Justifications for OWL DL
Entailments.
In John Domingue and Chutiporn Anutariya, editors, Proceedings of the 3th
Asian Semantic Web Conference (ASWC'08), volume 5367 of Lecture
Notes in Computer Science, pages 1–15. Springer-Verlag, 2008.
Bibtex entry Paper (PDF) ©Springer-Verlag
Abstract
Finding the justifications for an entailment (i.e., minimal sets of axioms responsible for it) is a prominent reasoning service in ontology engineering, as justifications facilitate important tasks like debugging inconsistencies or undesired subsumption. Though several algorithms for finding all justifications exist, issues concerning efficiency and scalability remain a challenge due to the sheer size of real-life ontologies. In this paper, we propose a novel method for finding all justifications in OWL DL ontologies by limiting the search space to smaller modules. To this end, we show that so-called locality-based modules cover all axioms in the justifications. We present empirical results that demonstrate an improvement of several orders of magnitude in efficiency and scalability of finding all justifications in OWL DL ontologies.
Quoc Huy Vu.
Subsumption in the Description Logic in ELHIf_R^+
w.r.t. General TBoxes.
Master thesis, TU Dresden, Germany, 2008.
Bibtex
entry Paper
(PDF)
Abstract
Description Logics are a family of knowledge representation formalisms for representing and reasoning about conceptual knowledge. Every DL system has reasoning services as an important component that infer implicit knowledge from the one explicitly given. Standard reasoning problems include concept satisability, concept subsumption, ABox consistency and the instance checking problem. This work considers the concept subsumption service, which is considered to be the most \traditional" service.
Four years ago, a polynomial time algorithm for subsumption problem in the Description Logic EL was developed. After that, algorithms for dierent problems in tractable extensions of EL have been developing. These Description Logics are sucient to represent many knowledge bases; however, there are ontologies requiring more expressive extensions of EL. Specifically, GALEN, an important medical ontology, requires ELHIfR+, an intractable extension of EL that includes role hierarchies, inverse , functional and transitive roles. This motivates the extension of the polynomial time algorithm to ELHIfR+.
This thesis proposes two solutions for the subsumption problem in ELHIfR+. The rst solution is to reduce ELHIfR+ to the less expressive DL ELI, for which an algorithm is readily available. The second solution is to create an algorithm for the concept subsumption problem in ELHIfR+. This algorithmstill runs in polynomial time in the simple case of ELHIfR+ that does not include inverse and functional roles.
Back to the homepage of the Chair for Automata Theory.
Generated at Fri Mar 19 16:53:03 CET 2010.