Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Technical Reports
2012
Franz Baader and Alexander Okhotin.
Solving Language Equations and Disequations Using Looping Tree Automata
with Colors.
LTCS-Report 12-01, Chair of Automata Theory, Institute of Theoretical Computer
Science, Technische Universität Dresden, Dresden, Germany, 2012.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
We extend previous results on the complexity of solving language equations with one-sided
concatenation and all Boolean operations to the case where also disequations (i.e.,
negated equations) may occur. To show that solvability of systems of equations and
disequations is still in ExpTime, we introduce a new type of automata working on infinite
trees, which we call looping automata with colors. As applications of these results, we
show new complexity results for disunification in the description logic FL0 and for
monadic set constraints with negation. We believe that looping automata with colors
may also turn out to be useful in other applications.
Franz Baader, Stefan Borgwardt, and Barbara Morawska.
SAT Encoding of Unification in ELH_R^+ w.r.t.
Cycle-Restricted Ontologies.
LTCS-Report 12-02, Chair for Automata Theory, Institute for Theoretical
Computer Science, Technische Universität Dresden, Dresden, Germany, 2012.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
Unification in Description Logics has been proposed as an inference service that can,
for example, be used to detect redundancies in ontologies. For the Description Logic EL,
which is used to define several large biomedical ontologies, unification is NP-complete.
An NP unification algorithm for EL based on a translation into propositional
satisfiability (SAT) has recently been presented. In this report, we extend this SAT
encoding in two directions: on the one hand, we add general concept inclusion axioms,
and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the
translation to be complete, however, the ontology needs to satisfy a certain cycle
restriction. The SAT translation depends on a new rewriting-based characterization of
subsumption w.r.t. ELHR+-ontologies.
Franz Baader, Stefan Borgwardt, and Barbara Morawska.
Computing Minimal EL-Unifiers is Hard.
LTCS-Report 12-03, Chair for Automata Theory, Institute for Theoretical
Computer Science, Technische Universität Dresden, Dresden, Germany, 2012.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
Unification has been investigated both in modal logics and in description logics,
albeit with different motivations. In description logics, unification can be used
to detect redundancies in ontologies. In this context, it is not sufficient to decide
unifiability, one must also compute appropriate unifiers and present them to the user.
For the description logic EL, which is used to define several large biomedical
ontologies, deciding unifiability is an NP-complete problem. It is known that every
solvable EL-unification problem has a minimal unifier, and that every
minimal unifier is a local unifier. Existing unification algorithms for EL
compute all minimal unifiers, but additionally (all or some) non-minimal local unifiers.
Computing only the minimal unifiers would be better since there are considerably
less minimal unifiers than local ones, and their size is usually also quite small.
In this paper we investigate the question whether
the known algorithms for EL-unification can be modified such that they
compute exactly the minimal unifiers without changing the complexity and the basic
nature of the algorithms. Basically, the answer we give to this question is negative.
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.