Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Technical Reports
2009
Conrad Drescher, Hongkai Liu, Franz Baader, Steffen Guhlemann, Uwe Petersohn,
Peter Steinke, and Michael Thielscher.
Putting ABox Updates into Action.
LTCS-Report 09-01, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2009.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
When trying to apply recently developed approaches for updating Description Logic ABoxes
in the context of an action programming language, one encounters two problems.
First, updates generate so-called Boolean ABoxes, which cannot be handled by traditional
Description Logic reasoners.
Second, iterated update operations result in very large Boolean ABoxes, which, however, contain
a huge amount of redundant information.
In this paper, we address both issues from a practical point of view.
Franz Baader, Martin Knechtel, and Rafael Peñaloza.
Computing Boundaries for Reasoning in Sub-Ontologies.
LTCS-Report 09-02, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2009.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
Consider an ontology O where every axiom is labeled with an element of
a lattice L. Then every element l of L determines a sub-ontology O_l,
which consists of the axioms of O whose labels are greater or equal to
l. These labels may be interpreted as required access rights, in which
case O_l is the sub-ontology that a user with access right l is
allowed to see, or as trust levels, in which case O_l consists of
those axioms that we trust with level at least l. Given a consequence
C (such as a subsumption relationship between concepts) that follows
from the whole ontology O, we want to know from which of the
sub-ontologies O_l, determined by lattice elements l, C still follows.
However, instead of reasoning with O_l in the deployment phase of the
ontology, we want to pre-compute this information during the
development phase. More precisely, we want to compute what we call a
boundary for C, i.e., an element m_C of L such that C follows from O_l
iff l is smaller or equal to m_C.
In this paper we show that, under certain restrictions on the elements
l used to define the sub-ontologies, such a boundary always exists,
and we describe black-box approaches for computing it that are
generalizations of approaches for axiom pinpointing in description
logics. We also present first experimental results that compare the
efficiency of these approaches on real-world ontologies.
Franz Baader, Hongkai Liu, and Anees ul Mehdi.
Integrate Action Formalisms into Linear Temporal Description
Logics.
LTCS-Report 09-03, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2009.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
The verification problem for action logic programs with non-terminating behaviour is in general undecidable. In this paper, we consider a restricted setting in which the problem becomes decidable. On the one hand, we abstract from the actual execution sequences of a non-terminating program by considering infinite sequences of actions defined by a B\"uchi automaton. On the other hand, we assume that the logic underlying our action formalism is a decidable description logic rather than full first-order predicate logic.
Rafael Peñaloza and Baris Sertkaya.
On the Complexity of Axiom Pinpointing in Description Logics.
LTCS-Report 09-04, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2009.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
We investigate the computational complexity of axiom pinpointing in Description
Logics, which is the task of finding minimal subsets of a knowledge base that
have a given consequence. We consider the problems of enumerating such subsets
with and without order, and show hardness results
that already hold for the propositional Horn fragment, or for the Description
Logic \EL. We show complexity results for several other related decision and
enumeration problems for these fragments that extend to more expressive logics.
In particular we show that hardness of these problems depends not
only on expressivity of the fragment but also on the shape of the axioms used.
There is also a complete overview of our technical reports.
Back to the homepage of the Chair for Automata Theory.
Generated at Mon Jan 30 16:30:34 CET 2012.