Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Publications
2002
C. Areces and C. Lutz.
Concrete Domains and Nominals United..
In Carlos Areces, Patrick Blackburn, Maarten Marx, and Ulrike Sattler, editors,
Proceedings of the fourth Workshop on Hybrid Logics (HyLo'02), 2002.
Bibtex entry Paper (PS)
Abstract
While the complexity of concept satisfiability in both ALCO, the basic description logic ALC enriched with nominals, and ALC(D), the extension of ALC with concrete domains, is known
to be PSpace-complete, in this article we show that the combination ALCO(D) of these two logics can have a NExpTime-hard concept satisfiability problem (depending on the concrete
domain D used). The proof is by a reduction of a NExpTime-complete variant of the domino problem to ALCO(D)-concept satisfiability.
F. Baader, I. Horrocks, and U. Sattler.
Description Logics for the Semantic Web.
KI – Künstliche Intelligenz, 4, 2002.
Bibtex entry Abstract
Abstract
The vision of a Semantic Web has recently drawn considerable
attention, both from academia and industry. Description Logics
are often named as one of the tools that can support the Semantic
Web and thus help to make this vision reality.
In this paper, we try to sketch what Description Logics are and
what they can do for the Semantic Web. It turns out that
Descriptions Logics are very useful for defining ontologies,
which provide the Semantic Web with a common understanding of
the basic semantic concepts used to annotate Web pages.
We also argue that, without the last decade of basic research
in this area, Description Logics could not play such an important
role in this domain.
F. Baader and R. Küsters.
Unification in a Description Logic with Inconsistency and Transitive
Closure of Roles.
In I. Horrocks and S. Tessaris, editors, Proceedings of the 2002
International Workshop on Description Logics, Toulouse, France, 2002.
See http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-53/.
Bibtex entry Paper (PS)
Abstract
Unification considers concept patterns, i.e., concept descriptions with
variables, and tries to make these descriptions equivalent by replacing the
variables by appropriate concept descriptions. In a previous paper, we have
shown that unification in FLreg, a description logic that allows for the
concept constructors top concept, concept conjunction, and value restrictions
as well as the role constructors union, composition, and transitive closure,
is an ExpTime-complete problem and that solvable FLreg-unification problems
always have least unifiers. In the present paper, we generalize these results
to a DL which extends FLreg by the bottom concept. The proof strongly
depends on the existence of least unifiers in FLreg.
F. Baader, C. Lutz, H. Sturm, and F. Wolter.
Fusions of Description Logics and Abstract Description Systems.
Journal of Artificial Intelligence Research (JAIR), 16:1–58, 2002.
Bibtex entry Paper (PS)
Abstract
Fusions are a simple way of combining logics. For normal modal logics, fusions
have been investigated in detail. In particular, it is known that, under
certain conditions, decidability transfers from the component logics to their
fusion. Though description logics are closely related to modal logics, they
are not necessarily normal. In addition, ABox reasoning in description logics
is not covered by the results from modal logics.
In this paper, we extend the decidability transfer results from normal modal
logics to a large class of description logics. To cover different description
logics in a uniform way, we introduce abstract description systems, which can
be seen as a common generalization of description and modal logics, and show
the transfer results in this general setting.
F. Baader and C. Tinelli.
Combining Decision Procedures for Positive Theories Sharing
Constructors.
In S. Tison, editor, Proceedings of the 13th International Conference on
Rewriting Techniques and Applications (RTA-02), volume 2378 of
Lecture Notes in Computer Science, pages 338–352, Copenhagen, Denmark,
2002. Springer-Verlag.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
This paper addresses the following combination problem:
given two equational theories E1 and E2 whose positive
theories are decidable, how can one obtain a decision
procedure for the positive theory of their union.
For theories over disjoint signatures, this problem was
solved by Baader and Schulz in 1995.
This paper is a first step towards extending this result to the
case of theories sharing constructors.
Since there is a close connection between
positive theories and unification problems, this also extends
to the non-disjoint case the work on combining decision procedures
for unification modulo equational theories.
F. Baader and C. Tinelli.
Deciding the Word Problem in the Union of Equational Theories.
Information and Computation, 178(2):346–390, 2002.
Bibtex entry Free reprint
Abstract
The main contribution of this article is a new method for
combining decision procedures for the word problem in equational
theories. In contrast to previous methods, it is based on
transformation rules, and also applies to theories sharing
"constructors."
F. Baader and A.-Y. Turhan.
On the problem of computing small representations of least common
subsumers.
In Proceedings of the German Conference on Artificial Intelligence, 25th
German Conference on Artificial Intelligence (KI 2002), Lecture Notes in
Artificial Intelligence, Aachen, Germany, 2002. Springer–Verlag.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
For Description Logics with existential restrictions, the size of
the least common subsumer (lcs) of concept descriptions may grow
exponentially in the size of the input descriptions. The first
(negative) result presented in this paper is that it is in general
not possible to express the exponentially large concept description
representing the lcs in a more compact way by using an appropriate
(acyclic) terminology.
In practice, a second and often more severe cause of complexity
was the fact that concept descriptions containing concepts defined
in a terminology must first be unfolded (by replacing defined names
by their definition) before the known lcs algorithms could be applied.
To overcome this problem, we present a modified lcs algorithm
that performs lazy unfolding, and show that this algorithm works
well in practice.
S. Brandt, R. Küsters, and A.-Y. Turhan.
Approximating ALCN-Concept Descriptions.
In Proceedings of the 2002 International Workshop on Description
Logics, 2002.
Bibtex entry Paper (PS)
Abstract
Approximating a concept, defined in one DL, means to translate this
concept to another concept, defined in a second typically less
expressive DL, such that both concepts are as closely related as
possible with respect to subsumption. In a previous work, we have
provided an algorithm for approximating ALC-concept descriptions by
ALE-concept descriptions. In the present paper, motivated by an
application in chemical process engineering, we extend this result by
taking number restrictions into account.
S. Brandt, R. Küsters, and A.-Y. Turhan.
Approximation and Difference in Description Logics.
In D. Fensel, F. Giunchiglia, D. McGuiness, and M.-A. Williams, editors,
Proceedings of the Eighth International Conference on Principles of Knowledge
Representation and Reasoning (KR2002), pages 203–214, San Francisco, CA,
2002. Morgan Kaufman.
Bibtex entry Paper (PS)
Abstract
Approximation is a new inference service in Description Logics first mentioned
by Baader, Küsters, and Molitor. Approximating a concept, defined in one
Description Logic, means to translate this concept to another concept, defined
in a second typically less expressive Description Logic, such that both
concepts are as closely related as possible with respect to subsumption. The
present paper provides the first in-depth investigation of this inference
task. We prove that approximations from the Description Logic ALC to ALE
always exist and propose an algorithm computing them.
As a measure for the accuracy of the approximation, we introduce a
syntax-oriented difference operator, which yields a concept that contains all
aspects of the approximated concept that are not present in the approximation.
It is also argued that a purely semantical difference operator, as introduced
by Teege, is less suited for this purpose. Finally, for the logics under
consideration, we propose an algorithm computing the difference.
S. Brandt and A.-Y. Turhan.
An Approach for Optimized Approximation.
In Proceedings of the KI-2002 Workshop on Applications of Description
Logics (KIDLWS'01), CEUR-WS, Aachen, Germany, September 2002. RWTH
Aachen.
Proceedings online available from
http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/.
Bibtex entry Paper (PS)
Abstract
Approximation is a new inference service investigated in
[BKT-KR-02]. An approximation of an ALC-concept by an ALE-concept
can be computed in double exponential time. Consequently, one needs
powerful optimization techniques for approximating an entire
unfoldable TBox. Addressing this issue we identify a special form of
ALC-concepts that can be divided into parts s.t.\ each part can be
approximated independently.
S. Demri and U. Sattler.
Automata-Theoretic Decision Procedures for Information Logics.
Fundamenta Informaticae, 53(1):1–22, 2002.
Bibtex entry Paper (PS)
T. Hinze.
Universelle Modelle und ausgewählte Algorithmen des DNA-Computing.
PhD thesis, Technische Universität Dresden, 2002.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
Die Arbeit beleuchtet das Forschungsgebiet des DNA-Computing vordergründig
aus dem Blickwinkel der Berechenbarkeitstheorie. Universelle sowie
platzbeschränkt universelle Modelle des DNA-Computing, deren DNA-basierte
Daten auf der Abbildung linearer DNA beruhen, werden untersucht,
klassifiziert und als Beschreibungssysteme für Algorithmen angewendet. Mit
dem TT6-EH-System und dem Simulationssystem Sisyphus werden zwei
universelle DNA-Computing-Modelle eingeführt, deren Modelleigenschaften
labornah ausgerichtet sind. Das TT6-EH-System stellt ein
endlichkomponentiges verteiltes Splicing-System dar, das sich durch einen
statischen Systemaufbau, eine Minimierung der in die Verarbeitung
einbezogenen Ressourcen und ein niedriges Abstraktionsniveau der
Modelloperationen auszeichnet. Das Simulationssystem Sisyphus
berücksichtigt Seiteneffekte der den Modelloperationen zugrundeliegenden
molekularbiologischen Prozesse. Zusätzlich besitzt das Modell die
Eigenschaften "restriktiv" und "multimengenbasiert". Anhand einer
Probleminstanz des NP-vollständigen Rucksackproblems erfolgte eine
laborpraktische Verifikation.
T. Hinze, U. Hatnik, and M. Sturm.
An Object Oriented Simulation of Real Occurring Molecular Biological
Processes for DNA Computing and Its Experimental Verification.
In N. Jonoska and N.C. Seeman, editors, DNA Computing. Proceedings Seventh
International Workshop on DNA-Based Computers (DNA7) Tampa, FL, USA,
2001, volume 2340 of Series Lecture Notes in Computer Science.
Springer Verlag, 2002.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag
Abstract
We present a simulation tool for frequently used DNA operations on
the molecular level including side effects based on a probabilistic
approach. The specification of the considered operations is
directly adapted from detailed observations of molecular
biological processes in laboratory studies. Bridging the gap between
formal models of DNA computing, we use process description methods
from biochemistry and show the closeness of the simulation to the
reality.
J. Hladik.
Implementation and evaluation of a tableau algorithm for the Guarded
Fragment.
In I. Horrocks and S. Tessaris, editors, Proceedings of the 2002
international workshop on description Logics (DL 2002), volume 53 of
CEUR, Toulouse, France, 2002.
Bibtex entry Paper (PS)
Abstract
In this paper we present SAGA, an implementation of a tableau-based
Satisfiability Algorithm for the Guarded
Fragment (GF). Satisfiability for GF with finite signature is
ExpTime-complete and therefore intractable in the worst case, but existing
tableau-based systems for ExpTime-complete description and modal logics
perform reasonably well for ``realistic'' knowledge bases. We implemented
and evaluated several optimizations used in description logic systems, and
our results show that, with an efficient combination, SAGA can compete with
existing highly optimized systems for description logics.
J. Hladik.
Implementation and Optimisation of a Tableau Algorithm for the Guarded
Fragment.
In U. Egly and C. G. Fermüller, editors, Proceedings of the International
Conference on Automated Reasoning with Tableaux and Related Methods (Tableaux
2002), volume 2381 of Lecture Notes in Artificial Intelligence.
Springer-Verlag, 2002.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
In this paper, we present SAGA, the implementation of a tableau-based
Satisfiability Algorithm for the Guarded
Fragment (GF). Satisfiability for GF with finite signature is
Exptime-complete and therefore theoretically intractable, but existing
tableau-based systems for Exptime-complete description and modal logics
perform well for many realistic knowledge bases. We implemented and
evaluated several optimisations used in description logic systems,
and our results show that with an efficient combination, SAGA can compete
with existing highly optimised systems for description logics and first
order logic.
I. Horrocks and U. Sattler.
Optimised Reasoning for SHIQ.
In Proc. of the 15th European Conference on Artificial Intelligence,
2002.
Bibtex entry Paper (PS) Paper (PDF)
O. Kupferman, U. Sattler, and M. Y. Vardi.
The Complexity of the Graded mu-Calculus.
In Proceedings of the Conference on Automated Deduction, volume 2392 of
Lecture Notes in Artificial Intelligence. Springer Verlag, 2002.
Bibtex entry Paper (PS) ©Springer-Verlag
C. Lutz.
Adding Numbers to the SHIQ Description Logic—First
Results.
In Proceedings of the Eighth International Conference on Principles of
Knowledge Representation and Reasoning (KR2002). Morgan Kaufman, 2002.
To appear.
Bibtex entry Paper (PS)
Abstract
Recently, the Description Logic (DL) SHIQ has found a large number of
applications. This success is due to the fact that SHIQ combines a rich
expressivity with efficient reasoning, as is demonstrated by its
implementation in DL systems such as FaCT and RACER. One weakness of SHIQ,
however, limits its usability in several application areas: numerical
knowledge such as knowledge about the age, weight, or temperature of
real-world entities cannot be adequately represented. In this paper, we
propose an extension of SHIQ that aims at closing this gap. The new
Description Logic Q-SHIQ, which augments SHIQ by additional, "concrete domain"
style concept constructors, allows to refer to rational numbers in concept
descriptions, and also to define concepts based on the comparison of numbers
via predicates such as "<" "=". We argue that this kind of expressivity is
needed in many application areas such as reasoning about the semantic web. We
prove reasoning with Q-SHIQ to be ExpTime-complete (thus not harder than
reasoning with SHIQ) by devising an automata-based decision procedure.
C. Lutz.
Description Logics with Concrete Domains—A Survey.
In Advances in Modal Logic 2002 (AiML 2002), Toulouse, France, 2002.
Final version appeared in Advanced in Modal Logic Volume 4, 2003.
Bibtex entry Paper (PS)
Abstract
Description logics (DLs) are a family of logical formalisms that
have initially been designed for the representation of conceptual
knowledge in artificial intelligence and are closely related to
modal logics. In the last two decades, DLs have been successfully
applied in a wide range of interesting application areas. In most of
these applications, it is important to equip DLs with expressive
means that allow to describe ``concrete qualities'' of real-world
objects such as their weight, temperature, and spatial extension.
The standard approach is to augment description logics with
so-called concrete domains, which consist of a set (say, the
rational numbers), and a set of n-ary predicates with a fixed
extension over this set. The ``interface'' between the DL and the
concrete domain is then provided by a new logical constructor that
has, to the best of our knowledge, no counterpart in modal logics.
In this paper, we give an overview over description logics with
concrete domains and summarize decidability and complexity results
from the literature.
C. Lutz.
PSpace Reasoning with the Description Logic
ALCF(D).
Logic Journal of the IGPL, 10(5):535–568, 2002.
Bibtex entry Paper (PS)
Abstract
Description Logics (DLs), a family of formalisms for reasoning about
conceptual knowledge, can be extended with concrete domains
to allow an adequate representation of "concrete qualities" of
real-worlds entities such as their height, temperature, duration,
and size. In this paper, we study the complexity of reasoning with
the basic DL with concrete domains ALC(D) and its extension with
so-called feature agreements and disagreements ALCF(D). We show that,
for both logics, the standard reasoning tasks concept
satisfiability, concept subsumption, and ABox consistency are
PSpace-complete if the concrete domain D satisfies some natural
conditions.
C. Lutz.
Reasoning about Entity Relationship Diagrams with Complex Attribute
Dependencies.
In Proceedings of the 2002 International Workshop on Description
Logics, 2002.
To appear.
Bibtex entry Paper (PS)
Abstract
Entity Relationship (ER) diagrams are among the most popular formalisms for
the support of database design. To aid database designers in building
(extended) ER schemas, Description Logics (DLs) have been proposed and
successfully used as a tool for reasoning about such schemas. In this paper,
we propose the extension of ER diagrams with dependencies on attributes and
show how such dependencies can be translated into DLs with concrete domains.
The result is an integrated approach to reasoning with conceptual models and
attribute dependencies.
C. Lutz and U. Sattler.
A Proposal for Describing Services with DLs.
In Proceedings of the 2002 International Workshop on Description
Logics, 2002.
To appear.
Bibtex entry Paper (PS)
Abstract
Motivated by the semantic web application, we present a generic extension of
description logics to describe actions. These actions can then be chained to
service descriptions. A web page providing a service can be annotated with a
description of this service, which can then be taken into account by agents
searching for a web service. Besides defining syntax and semantics of this
extension of DLs, we introduce and discuss inference problems which are useful
to annotate web pages with a description of the service they provide.
C. Lutz, H. Sturm, F. Wolter, and M. Zakharyaschev.
A Tableau Decision Algorithm for Modalized ALC with Constant
Domains.
Studia Logica, 72(2):199–232, 2002.
Bibtex entry Paper (PDF)
Abstract
The aim of this paper is to construct a tableau decision algorithm for the
modal description logic K/ALC with constant domains. More precisely, we
present a tableau procedure that is capable of deciding, given an ALC-formula
x with extra modal operators (which are applied only to concepts and TBox
axioms, but not to roles), whether x is satisfiable in a model with constant
domains and arbitrary accessibility relations. Tableau-based algorithms have
been shown to be `practical' even for logics of rather high complexity. This
gives us grounds to believe that, although the satisfiability problem for
K/ALC is known to be NEXPTIME-complete, by providing a tableau decision
algorithm we demonstrate that highly expressive description logics with modal
operators have a chance to be implementable. The paper gives a solution to an
open problem of Baader and Laux.
G. Pan, U. Sattler, and M. Y. Vardi.
BDD-Based Decision Procedures for K.
In Proceedings of the Conference on Automated Deduction, volume 2392 of
Lecture Notes in Artificial Intelligence. Springer Verlag, 2002.
Bibtex entry Paper (PS) ©Springer-Verlag
Back to the homepage of the Chair for Automata Theory.
Generated at Mon Apr 30 13:36:07 CEST 2012.