Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Publications
2000
F. Baader and R. Küsters.
Matching in Description Logics with Existential Restrictions.
In A.G. Cohn, F. Giunchiglia, and B. Selman, editors, Proceedings of the
Seventh International Conference on Knowledge Representation and Reasoning (KR2000), pages 261–272, San Francisco, CA, 2000. Morgan Kaufmann
Publishers.
Bibtex entry Paper (PS)
Abstract
Matching of concepts against patterns is a
new inference task in Description Logics, which was
originally motivated by applications of the CLASSIC
system. Consequently, the work on this problem
was until now mostly concerned with sublanguages of the
CLASSIC language, which does not allow for
existential restrictions.
This paper extends the existing work on matching in two directions. On the one
hand, the question of what are the most ``interesting" solutions of matching
problems is explored in more detail. On the other hand, for languages with
existential restrictions both, the complexity of deciding the solvability of
matching problems and the complexity of actually computing sets of
``interesting" matchers are determined. The results show that existential
restrictions make these computational tasks more complex. Whereas for
sublanguages of CLASSIC both problems could be solved in polynomial time, this
is no longer possible for languages with existential restrictions.
F. Baader, R. Küsters, and R. Molitor.
Rewriting Concepts Using Terminologies.
In A.G. Cohn, F. Giunchiglia, and B. Selman, editors, Proceedings of the
Seventh International Conference on Knowledge Representation and Reasoning (KR2000), pages 297–308, San Francisco, CA, 2000. Morgan Kaufmann
Publishers.
Bibtex entry Paper (PS)
Abstract
The problem of rewriting a concept given a terminology can informally be stated
as follows: given a terminology T (i.e., a set of concept definitions) and a
concept description C that does not contain concept names defined in T, can this
description be rewritten into a related "better" description E by using (some
of) the names defined in T?
In this paper, we first introduce a general framework for the rewriting problem
in description logics, and then concentrate on one specific instance of the
framework, namely the minimal rewriting problem (where "better" means shorter,
and "related" means equivalent). We investigate the complexity of the decision
problem induced by the minimal rewriting problem for the languages FL0, ALN,
ALE, and ALC, and then introduce an algorithm for computing (minimal) rewritings
for the language ALE. (In the full paper, a similar algorithm is also developed
for ALN.) Finally, we sketch other interesting instances of the framework.
Our interest for the minimal rewriting problem stems from the fact that
algorithms for non-standard inferences, such as computing least common subsumers
and matchers, usually produce concept descriptions not containing defined
names. Consequently, these descriptions are rather large and hard to read and
comprehend. First experiments in a chemical process engineering application show
that rewriting can reduce the size of concept descriptions obtained as least
common subsumers by almost two orders of magnitude.
F. Baader, C. Lutz, H. Sturm, and F. Wolter.
Fusions of Description Logics.
In F. Baader and U. Sattler, editors, Proceedings of the International
Workshop in Description Logics 2000 (DL2000), number 33 in CEUR-WS,
pages 21–30, Aachen, Germany, August 2000. RWTH Aachen.
Proceedings online available from
http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-33/.
Bibtex entry Paper (PS)
Abstract
One of the major topics in Description Logic (DL) research is investigating
the trade-off between the expressivity of a DL and the complexity of its
inference problems. The expressiveness of a DL is usually determined by the
constructors available for building concepts and roles. Given two DLs, their
union is the DL that allows the unrestricted use of the constructors of both
DLs. There are well-known examples that show that decidability of DLs usually
does not transfer to their union.
In this paper, we consider the fusion of two DLs, which is more restrictive
than the union. Intuitively, in the fusion the role names are partitioned into
two sets, and the constructors of the first DL can only use role names of one
set, whereas the constructors of the second DL can only use role names of the
other set. We show that under certain (rather weak) conditions decidability
transfers from given DLs to their fusion. More precisely, the inference
problems that we consider are satisfiability/subsumption of concept
descriptions as well as satisfiability/subsumption w.r.t. general inclusion
axioms.
These results adapt and generalize known transfer results from modal logic to
DL. In order to capture the notion of a DL formally, we introduce the notion
of an abstract description system and prove our results within this new formal
framework.
F. Baader and R. Molitor.
Building and Structuring Description Logic Knowledge Bases Using Least
Common Subsumers and Concept Analysis.
In B. Ganter and G. Mineau, editors, Conceptual Structures: Logical,
Linguistic, and Computational Issues – Proceedings of the 8th International
Conference on Conceptual Structures (ICCS2000), volume 1867 of
Lecture Notes in Artificial Intelligence, pages 290–303. Springer
Verlag, 2000.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
Given a finite set C:={c_1, ... , c_n} of description logic concepts, we are
interested in computing the subsumption hierarchy of all least common subsumers
of subsets of C. This hierarchy can be used to support the bottom-up
construction and the structuring of description logic knowledge bases. The
point is to compute this hierarchy without having to compute the least common
subsumer for all subsets of C. In this paper, we show that methods from formal
concept analysis developed for computing concept lattices can be employed for
this purpose.
F. Baader and U. Sattler.
Tableau Algorithms for Description Logics.
In R. Dyckhoff, editor, Proceedings of the International Conference on
Automated Reasoning with Tableaux and Related Methods (Tableaux 2000),
volume 1847 of Lecture Notes in Artificial Intelligence, pages 1–18,
St Andrews, Scotland, UK, 2000. Springer-Verlag.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
Description logics are a family of knowledge representation
formalisms that are descended from semantic networks and frames
via the system KLONE. During the last decade, it has been shown
that the important reasoning problems (like subsumption and
satisfiability) in a great variety of description logics can be
decided using tableau-like algorithms. This is not very surprising
since description logics have turned out to be closely related
to propositional modal logics and logics of programs (such as
propositional dynamic logic), for which tableau procedures have
been quite successful.
Nevertheless, due to different underlying intuitions and
applications, most description logics differ significantly from
run-of-the-mill modal and program logics. Consequently, the research
on tableau algorithms in description logics led to new techniques
and results, which are, however, also of interest for modal logicians.
In this article, we will focus on three features that play an important
role in description logics (number restrictions, terminological
axioms, and role constructors), and show how they can be taken into
account by tableau algorithms.
F. Baader and C. Tinelli.
Combining Equational Theories Sharing Non-Collapse-Free Constructors.
In H. Kirchner and Ch. Ringeissen, editors, Proceedings of the 3rd
International Workshop on Frontiers of Combining Systems (FroCoS 2000),
volume 1794 of Lecture Notes in Computer Science, pages 257–271,
Nancy, France, 2000. Springer-Verlag.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
In this paper we extend the applicability of our combination
method for decision procedures for the word problem to theories
sharing non-collapse-free constructors.
This extension broadens the scope of the combination procedure
considerably, for example in the direction of equational theories
axiomatizing the equivalence of modal formulae.
S. Brandt.
Matching under Side Conditions in Description Logics.
Diploma thesis, RWTH Aachen, Germany, 2000.
Bibtex entry Paper (PS)
Abstract
Matching in Description Logics originally has been inroduced by Borgida and
McGuinness in order to prune aspects of concept descriptions irrelevant under
certain circumstances. In this context, side conditions have been proposed to
avoid trivial solutions to matching problems.
In this work the computational complexity of matching algorithms is discussed
for four common description logics---ALN and three of its sublanguages. Three
different problems are considered. Matching modulo equivalence without side
conditions, the approach of eliminating acyclic subsumption conditions and the
use of fixed point algorithms for solving matching problems under subsumption
conditions.
As a result, we prove that matching under subsumption conditions can be solved
in polynomial time in ALN and its sublanguages.
E. Franconi, F. Baader, U. Sattler, and P. Vassiliadis.
Multidimensional Data Models and Aggregation.
In M. Jarke, M. Lenzerini, Y. Vassilious, and P. Vassiliadis, editors,
Fundamentals of Data Warehousing, pages 87–106. Springer-Verlag, 2000.
Bibtex entry
T. Hinze and M. Sturm.
Towards an in-vitro Implementation of a Universal Distributed Splicing
Model for DNA Computation.
In R. Freund, editor, Proceedings Theorietag 2000 (TT2000) Wien, 2000.
Bibtex entry Paper (PS)
Abstract
Emphasizing a combination of recent developments in computer science
with molecular bioengineering, a special distributed splicing system
(TT6) is proposed. This unconventional model for computation
features by a possibility for an in-vitro implementation in the
laboratory as well as by a mathematical exact description. The
Dresden DNA Computation Group decided to implement such a system on
biohardware and optimized all relevant model parameters and
components with respect to this objective.
C. Hirsch and S. Tobies.
A Tableau Algorithm for the Clique Guarded Fragment.
In Proceedings of the Workshop Advances in Modal Logic AiML 2000,
Leipzig, Germany, 2000.
Final version appeared in Advanced in Modal Logic Volume 3, 2001.
Bibtex entry Paper (PS)
Abstract
We develop a tableau algorithm for the Clique Guarded Fragment (CGF), which we
hope can serve as basis for an efficient implementation of a decision
procedure for CGF. This hope is justified by the fact that some of the most
efficient implementations of modal or description logic reasoners are based on
tableau calculi similar to the one for CGF presented in this paper. As a
corollary from the constructions used to prove the correctness of the tableau
algorithm, we give an, in our opinion, simpler proof for the finite modal
property of the Guarded Fragment (GF). An extension of our approach to CGF is
part of future work. We also give a new proof of the fact that CGF and GF have
the generalised tree model property.
Jan Hladik.
Implementing the n-ary Description Logic GF1-.
In Proceedings of the International Workshop in Description Logics 2000
(DL2000), Aachen, Germany, 2000.
Bibtex entry Paper (PS)
Abstract
GF1- is a description logic allowing for n-ary relations, for which
satisfiability is decidable in PSPACE. In this paper, the implementation and
optimization of a tableau algorithm deciding GF1- are presented, and the
performance is compared with that of other solvers.
I. Horrocks, U. Sattler, S. Tessaris, and S. Tobies.
How to decide Query Containment under Constraints using a Description
Logic.
In Proceedings of the 7th International Workshop on Knowledge
Representation meets Databases (KRDB-2000), 2000.
Bibtex entry Paper (PS)
Abstract
Query containment under constraints is the problem of determining whether the
result of one query is contained in the result of another query for every
database satisfying a given set of constraints. This problem is of particular
importance in information integration and warehousing where, in addition to
the constraints derived from the source schemas and the global schema,
inter-schema constraints can be used to specify relationships between objects
in different schemas. A theoretical framework for tackling this problem using
the DLR logic has been established, and in this paper we show how the
framework can be extended to a practical decision procedure. The proposed
technique is to extend DLR with an Abox (a set of assertions about named
individuals and tuples), and to transform query subsumption problems into DLR
Abox satisfiability problems. We then show how such problems can be decided,
via a reification transformation, using a highly optimised reasoner for the
SHIQ description logic.
I. Horrocks, U. Sattler, S. Tessaris, and S. Tobies.
How to decide Query Containment under Constraints using a Description
Logic.
In Andrei Voronkov, editor, Proceedings of the 7th International Conference
on Logic for Programming and Automated Reasoning (LPAR'2000), number
1955 in Lecture Notes in Artificial Intelligence. Springer Verlag, 2000.
Bibtex entry Paper (PS)
Abstract
We present a procedure for deciding (database) query containment under
constraints. The technique is to extend the logic DLR with an Abox,
and to transform query subsumption problems into DLR Abox
satisfiability problems. Such problems can then be decided, via a
reification transformation, using a highly optimised reasoner for the
SHIQ description logic. We use a simple example to support our
hypothesis that this procedure will work well with realistic problems.
I. Horrocks, U. Sattler, and S. Tobies.
Practical Reasoning for Very Expressive Description Logics.
Logic Journal of the IGPL, 8(3):239–264, May 2000.
Bibtex entry Paper (PS)
Abstract
Description Logics (DLs) are a family of knowledge representation formalisms
mainly characterised by constructors to build complex concepts and roles from
atomic ones. Expressive role constructors are important in many applications,
but can be computationally problematical.
We present an algorithm that decides satisfiability of the DL ALC extended
with transitive and inverse roles and functional restrictions with respect to
general concept inclusion axioms and role hierarchies; early experiments
indicate that this algorithm is well-suited for implementation. Additionally,
we show that ALC extended with just transitive and inverse roles is still in
PSpace. We investigate the limits of decidability for this family of
DLs, showing that relaxing the constraints placed on the kinds of roles used
in number restrictions leads to the undecidability of all inference problems.
Finally, we describe a number of optimisation techniques that are crucial in
obtaining implementations of the decision procedures, which, despite the hight
worst-case complexity of the problem, exhibit good performance with real-life
problems.
I. Horrocks, U. Sattler, and S. Tobies.
Reasoning with Individuals for the Description Logic SHIQ.
In David MacAllester, editor, Proceedings of the 17th International
Conference on Automated Deduction (CADE-17), number 1831 in Lecture
Notes in Computer Science, Germany, 2000. Springer Verlag.
Bibtex entry Paper (PS)
Abstract
While there has been a great deal of work on the development of reasoning
algorithms for expressive description logics, in most cases only Tbox
reasoning is considered. In this paper we present an algorithm for combined
Tbox and Abox reasoning in the SHIQ description logic. This algorithm is of
particular interest as it can be used to decide the problem of (database)
conjunctive query containment w.r.t. a schema. Moreover, the realisation of an
efficient implementation should be relatively straightforward as it can be
based on an existing highly optimised implementation of the Tbox algorithm in
the FaCT system.
I. Horrocks and S. Tobies.
Optimisation of Terminological Reasoning.
In Proceedings of the International Workshop in Description Logics 2000
(DL2000), 2000.
Bibtex entry Paper (PS)
Abstract
When reasoning in description, modal or temporal logics it is often useful
to consider axioms representing universal truths in the domain of discourse.
Reasoning with respect to an arbitrary set of axioms is hard, even for
relatively inexpressive logics, and it is essential to deal with such axioms
in an efficient manner if implemented systems are to be effective in real
applications. This is particularly relevant to Description Logics, where
subsumption reasoning with respect to a terminology is a fundamental
problem. Two optimisation techniques that have proved to be particularly
effective in dealing with terminologies are lazy unfolding and absorption.
In this paper we seek to improve our theoretical understanding of these
important techniques. We define a formal framework that allows the
techniques to be precisely described, establish conditions under which they
can be safely applied, and prove that, provided these conditions are
respected, subsumption testing algorithms will still function correctly.
These results are used to show that the procedures used in the FaCT system
are correct and, moreover, to show how efficiency can be significantly
improved, while still retaining the guarantee of correctness, by relaxing
the safety conditions for absorption.
I. Horrocks and S. Tobies.
Reasoning with Axioms: Theory and Practice.
In A. G. Cohn, F. Giunchiglia, and B. Selman, editors, Principles of
Knowledge Representation and Reasoning: Proceedings of the Seventh
International Conference (KR2000), San Francisco, CA, 2000. Morgan
Kaufmann Publishers.
Bibtex entry Paper (PS)
Abstract
When reasoning in description, modal or temporal logics it is often useful
to consider axioms representing universal truths in the domain of discourse.
Reasoning with respect to an arbitrary set of axioms is hard, even for
relatively inexpressive logics, and it is essential to deal with such axioms
in an efficient manner if implemented systems are to be effective in real
applications. This is particularly relevant to Description Logics, where
subsumption reasoning with respect to a terminology is a fundamental
problem. Two optimisation techniques that have proved to be particularly
effective in dealing with terminologies are lazy unfolding and absorption.
In this paper we seek to improve our theoretical understanding of these
important techniques. We define a formal framework that allows the
techniques to be precisely described, establish conditions under which they
can be safely applied, and prove that, provided these conditions are
respected, subsumption testing algorithms will still function correctly.
These results are used to show that the procedures used in the FaCT system
are correct and, moreover, to show how efficiency can be significantly
improved, while still retaining the guarantee of correctness, by relaxing
the safety conditions for absorption.
C. Lutz.
NExpTime-Complete Description Logics with Concrete Domains.
In C. Pilière, editor, Proceedings of the ESSLLI-2000 Student
Session, University of Birmingham, August 2000.
Bibtex entry Paper (PS)
Abstract
Description Logics (DLs) are well-suited for the representation of abstract
conceptual knowledge. Concrete knowledge such as knowledge about numbers, time
intervals, and spatial regions can be incorporated into DLs by using so-called
concrete domains. The basic Description Logics providing concrete domains is
ALC(D) which was introduced by Baader and Hanschke. Reasoning with ALC(D)
concepts is known to be PSpace-complete if reasoning with the concrete domain
D is in PSpace. In this paper, we consider the extension of ALC(D) with acylic
TBoxes and inverse roles and examine the computational complexity of the
resulting formalism. As lower bounds, we show that there exists a concrete
domain P for which reasoning is in PTime such that reasoning with ALC(P) and
any of the above two extensions (separately) is NExpTime-hard. This is rather
surprising since acyclic TBoxes and inverse roles are known to ``usually'' not
increase the complexity of reasoning. For proving the lower bound, we
introduce a NExpTime-complete variant of the Post Correspondence Problem and
reduce it to the two logics under consideration. A corresponding upper bound,
which states that reasoning with ALC(D) and both above extensions (together)
is in NExpTime if reasoning with the concrete domain D is in NP, is proved
in the accompanying technical report.
C. Lutz and U. Sattler.
The Complexity of Reasoning with Boolean Modal Logic.
In Advances in Modal Logic 2000 (AiML 2000), Leipzig, Germany, 2000.
Final version appeared in Advanced in Modal Logic Volume 3, 2001.
Bibtex entry
C. Lutz and U. Sattler.
Mary likes all Cats.
In F. Baader and U. Sattler, editors, Proceedings of the 2000 International
Workshop in Description Logics (DL2000), number 33 in CEUR-WS, pages
213–226, Aachen, Germany, August 2000. RWTH Aachen.
Proceedings online available from
http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-33/.
Bibtex entry Paper (PS)
Abstract
We investigate the complexity of ALC with boolean operators on roles. Tight
complexity bounds are given for all logics between ALC with role negation and
ALC with full boolean operators on accessibility relations (also considering
restrictions to atomic role negation). More precisely, our main results are
tight bounds for
(1) ALC with role negation (which turns out to be ExpTime-complete),
(2) ALC with atomic role negation and role intersection (which turns out to be
NExpTime-complete, just like ALC with all boolean operators on roles).
Moreover, in order to demonstrate the generality of our results, we show that
the automata based techniques that were employed to obtain the upper bound for
(1) can be extended to obtain the same result for ALC extended with both
transitive roles and negation of roles.
R. Molitor and C.B. Tresp.
Extending Description Logics to Vague Knowledge in Medicine.
In P. Szczepaniak, P.J.G. Lisboa, and S. Tsumoto, editors, Fuzzy Systems in
Medicine, volume 41 of Studies in Fuzziness and Soft Computing,
pages 617–635. Springer Verlag, 2000.
Bibtex entry Abstract
Abstract
This work introduces a concept language that is an extension of classical
two-valued description logics to fuzzy logic. The new language allows to cope
with vague concepts, e.g., more or less enlarged liver or very small kidney
which are crucial notions in different medical application scenarios. To realize
the extension to fuzzy logic, the classical logical notions of satisfiability,
entailment and subsumption have to be modified appropriately. The main
contribution of this paper are sound and complete methods for computing
hierarchies between fuzzy concepts as well as processing queries in the new
fuzzy concept language. Furthermore, we give an introduction to a concrete
medical application that makes use of the fuzzy concept formalism.
U. Sattler.
Description Logics for the Representation of Aggregated Objects.
In W.Horn, editor, Proceedings of the 14th European Conference on
Artificial Intelligence. IOS Press, Amsterdam, 2000.
Bibtex entry Paper (PS)
E.P. Stoschek, M. Sturm, and T. Hinze et.al.
Molekularbiologisches Verfahren zur Lösung von NP-Problemen.
Deutsches Patent DE 198 53 726 A 1, IPC C12N 15/10, Deutsches Patentamt
München, 2000.
Bibtex entry
Stephan Tobies.
The Complexity of Reasoning with Cardinality Restrictions and Nominals in
Expressive Description Logics.
Journal of Artificial Intelligence Research, 12:199–217, May 2000.
Bibtex entry Paper (PS)
Abstract
We study the complexity of the combination of the Description Logics ALCQ
and ALCQI with a terminological formalism based on cardinality restrictions
on concepts. These combinations can naturally be embedded into C^2, the
two variable fragment of predicate logic with counting quantifiers, which
yields decidability in NExpTime. We show that this approach leads to an
optimal solution for ALCQI, as ALCQI with cardinality restrictions has the
same complexity as C^2 (NExpTime-complete). In contrast, we show that for
ALCQ, the problem can be solved in ExpTime. This result is obtained by a
reduction of reasoning with cardinality restrictions to reasoning with the
(in general weaker) terminological formalism of general axioms in the
presence of nominals in the language. Using the same reduction, we show that
for the extension of ALCQI with nominals reasoning with general axioms is a
NExpTime-complete problem. Finally, we sharpen this result and show that
already concept satisfiabiliy for ALCQI with nominals is
NExpTime-complete. Without nominals, this problem is known to be
PSPACE-complete.
Back to the homepage of the Chair for Automata Theory.
Generated at Mon Apr 30 13:36:07 CEST 2012.