Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Technical Reports
2011
Franz Baader, Nguyen Thanh Binh, Stefan Borgwardt, and Barbara Morawska.
Unification in the Description Logic EL Without the Top
Concept.
LTCS-Report 11-01, Chair of Automata Theory, Institute of Theoretical Computer
Science, Technische Universität Dresden, Dresden, Germany, 2011.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
Unification in Description Logics has been proposed as a novel inference
service that can, for example, be used to detect redundancies
in ontologies. The inexpressive Description Logic EL is of particular
interest in this context since, on the one hand, several large biomedical
ontologies are defined using EL. On the other hand, unification
in EL has recently been shown to be NP-complete, and thus
of considerably lower complexity than unification in other DLs of similarly
restricted expressive power.
However, EL allows the use of the top concept,
which represents the whole interpretation domain, whereas the large medical
ontology SNOMED CT makes no use of this feature. Surprisingly, removing
the top concept from EL makes the unification problem considerably
harder. More precisely, we will show in this paper that unification
in EL without the top concept is PSpace-complete.
Stefan Borgwardt and Rafael Peñaloza.
Complementation and Inclusion of Weighted Automata on Infinite Trees:
Revised Version.
LTCS-Report 11-02, Chair for Automata Theory, Institute for Theoretical
Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
Weighted automata can be seen as a natural generalization of finite state
automata to more complex algebraic structures. The standard reasoning tasks for
unweighted automata can also be generalized to the weighted setting. In this
report we study the problems of intersection, complementation, and inclusion for
weighted automata on infinite trees and show that they are not harder than
reasoning with unweighted automata. We also present explicit methods for solving
these problems optimally.
Rafael Peñaloza.
Towards a Tableau Algorithm for Fuzzy ALC with Product T-norm.
LTCS-Report 11-03, Chair for Automata Theory, Institute for Theoretical
Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
Very recently, the tableau-based algorithm for deciding consistency of general fuzzy DL ontologies over
the product t-norm was shown to be incorrect, due to a very weak blocking condition.
In this report we take the first steps towards a correct algorithm by modifying the blocking condition,
such that the (finite) structure obtained through the algorithm uniquely describes an infinite system of
quadratic constraints.
We show that this procedure terminates, and is sound and complete in the sense that the input is
consistent iff the corresponding infinite system of constraints is satisfiable.
Stefan Borgwardt and Barbara Morawska.
Finding Finite Herbrand Models.
LTCS-Report 11-04, Chair for Automata Theory, Institute for Theoretical
Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
We show that finding finite Herbrand models for a restricted class of
first-order clauses is ExpTime-complete. A Herbrand model is called finite if it
interprets all predicates by finite subsets of the Herbrand universe. The
restricted class of clauses consists of anti-Horn clauses with monadic
predicates and terms constructed over unary function symbols and constants.
The decision procedure can be used as a new goal-oriented algorithm to solve
linear language equations and unification problems in the description logic
FL_0. The new algorithm has only worst-case exponential runtime, in contrast to
the previous one which was even best-case exponential.
Franz Baader, Stefan Borgwardt, and Barbara Morawska.
Unification in the Description Logic EL w.r.t. Cycle-Restricted TBoxes.
LTCS-Report 11-05, Chair for Automata Theory, Institute for Theoretical
Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
Unification in Description Logics (DLs) has been proposed as an inference service that can, for
example, be used to detect redundancies in ontologies. The inexpressive Description Logic EL is
of particular interest in this context since, on the one hand, several large biomedical
ontologies are defined using EL. On the other hand, unification in EL has recently been shown to
be NP-complete, and thus of significantly lower complexity than unification in other DLs of
similarly restricted expressive power. However, the unification algorithms for EL developed so
far cannot deal with general concept inclusion axioms (GCIs). This paper makes a considerable
step towards addressing this problem, but the GCIs our new unification algorithm can deal with
still need to satisfy a certain cycle restriction.
Stefan Borgwardt and Rafael Peñaloza.
Undecidability of Fuzzy Description Logics.
LTCS-Report 11-06, Chair for Automata Theory, Institute for Theoretical
Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
Fuzzy description logics (DLs) have been investigated for over two decades, due to their
capacity to formalize and reason with imprecise concepts. Very recently, it has been shown that
for several fuzzy DLs, reasoning becomes undecidable. Although the proofs of these results
differ in the details of each specific logic considered, they are all based on the same basic
idea.
In this report, we formalize this idea and provide sufficient conditions for proving
undecidability of a fuzzy DL. We demonstrate the effectiveness of our approach by strengthening
all previously-known undecidability results and providing new ones. In particular, we show that
undecidability may arise even if only crisp axioms are considered.
There is also a complete overview of our technical reports.
Back to the homepage of the Chair for Automata Theory.
Generated at Tue Apr 24 10:46:19 CEST 2012.