Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Publications
2003
F. Baader.
Description Logic Terminology.
In Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and
Peter F. Patel-Schneider, editors, The Description Logic Handbook:
Theory, Implementation, and Applications, pages 485–495. Cambridge
University Press, 2003.
Bibtex entry Abstract
Abstract
The purpose of this appendix is to introduce (in a compact manner) the syntax
and semantics of the most prominent DLs occurring in this handbook. More
information and explanations as well as some less familiar DLs can be found
in the respective chapters. For DL constructors whose semantics cannot be
described in a compact manner, we will only introduce the syntax and refer
the reader to the respective chapter for the semantics. Following
Chapter~2 on Basic Description Logics, we will first introduce the basic DL
AL, and then describe several of its extensions. Thereby, we will also fix the
notation employed in this handbook.
F. Baader, J. Hladik, C. Lutz, and F. Wolter.
From Tableaux to Automata for Description Logics.
In Moshe Vardi and Andrei Voronkov, editors, Proceedings of the 10th
International Conference on Logic for Programming, Artificial Intelligence,
and Reasoning (LPAR 2003), volume 2850 of Lecture Notes in Computer
Science, pages 1–32. Springer, 2003.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
This paper investigates the relationship between automata- and tableau-based
inference procedures for Description Logics.
To be more precise, we develop an abstract notion of
what a tableau-based algorithm is, and then show, on this abstract level, how
tableau-based algorithms can be converted into automata-based
algorithms. In particular, this allows us to characterize a large class of
tableau-based algorithms that imply an ExpTime upper-bound for
reasoning in the description logics for which such an algorithm exists.
F. Baader, R Küsters, and F. Wolter.
Extensions to Description Logics.
In Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and
Peter F. Patel-Schneider, editors, The Description Logic Handbook:
Theory, Implementation, and Applications, pages 219–261. Cambridge
University Press, 2003.
Bibtex entry Abstract
Abstract
This chapter considers, on the one hand,
extensions of Description Logics by features not available in the basic
framework, but considered important for using Description Logics as a modeling language.
In particular, it addresses the extensions concerning: concrete domain constraints;
modal, epistemic, and temporal operators; probabilities and fuzzy logic; and defaults.
On the other hand, it considers non-standard inference problems for
Description Logics, i.e., inference problems that---unlike subsumption or instance
checking---are not available in all systems, but have turned out to be useful in
applications. In particular, it addresses the non-standard inference problems:
least common subsumer and most specific concept; unification and matching of concepts;
and rewriting.
F. Baader and W. Nutt.
Basic Description Logics.
In Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and
Peter F. Patel-Schneider, editors, The Description Logic Handbook:
Theory, Implementation, and Applications, pages 43–95. Cambridge
University Press, 2003.
Bibtex entry Abstract
Abstract
This chapter provides an introduction to Description Logics as a formal
language for representing knowledge and reasoning about it.
It first gives a short overview of the ideas underlying Description
Logics. Then it introduces syntax and semantics, covering the basic
constructors that are used in systems or have been introduced in
the literature, and the way these constructors can be used to build
knowledge bases. Finally, it defines the typical inference problems,
shows how they are interrelated, and describes different approaches for
effectively solving these problems. Some of the topics that are only
briefly mentioned in this chapter will be treated in more detail in
subsequent chapters.
F. Baader and U. Sattler.
Description Logics with Aggregates and Concrete Domains.
Information Systems, 28(8):979–1004, 2003.
Bibtex entry Paper (PS) Free reprint
Abstract
Description Logics are a family of knowledge representation
formalisms well-suited for intensional reasoning about conceptual
models of databases/data warehouses.
We extend Description Logics with concrete domains (such as integers
and rational numbers)
that include aggregation functions over these domains (such as
min, max, count, and sum) which are usually available in
database systems.
We show that the presence of aggregation functions may easily lead
to undecidability of (intensional) inference problems such as
satisfiability and subsumption.
However, there are also extensions for which satisfiability and
subsumption are decidable, and we present decision procedures for
the relevant inference problems.
Franz Baader.
Computing the least common subsumer in the description logic EL
w.r.t. terminological cycles with descriptive semantics.
In Proceedings of the 11th International Conference on Conceptual
Structures, ICCS 2003, volume 2746 of Lecture Notes in Artificial
Intelligence, pages 117–130. Springer-Verlag, 2003.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag
Abstract
Computing the least common subsumer (lcs) is one of the most prominent
non-standard inference in description logics. Baader, Kuesters, and
Molitor have shown that the lcs of concept descriptions in the description
logic EL always exists and can be computed in polynomial time.
In the present paper, we try to extend this result from concept
descriptions to concepts defined in a (possibly cyclic) EL-terminology
interpreted with descriptive semantics, which is the usual first-order
semantics for description logics. In this setting,
the lcs need not exist. However, we are able to define
possible candidates P_k (k\geq 0) for the lcs,
and can show that the lcs exists iff one of these candidates is
the lcs. Since each of these candidates is a common subsumer,
they can also be used to approximate the lcs even if it does not
exist. In addition, we give a sufficient condition for the
lcs to exist, and show that, under this condition,
it can be computed in polynomial time.
Franz Baader.
The instance problem and the most specific concept in the description logic
EL w.r.t. terminological cycles with descriptive semantics.
In Proceedings of the 26th Annual German Conference on Artificial
Intelligence, KI 2003, volume 2821 of Lecture Notes in Artificial
Intelligence, pages 64–78, Hamburg, Germany, 2003. Springer-Verlag.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
Previously, we have investigated both standard
and non-standard inferences in the presence of terminological cycles
for the description logic EL, which allows for conjunctions,
existential restrictions, and the top concept.
The present paper is concerned with two problems left open by
this previous work, namely the instance problem
and the problem of computing most specific concepts w.r.t. descriptive
semantics, which is the usual first-order semantics for
description logics.
We will show that---like subsumption---the instance problem is polynomial
in this context.
Similar to the case of the least common subsumer,
the most specific concept w.r.t. descriptive semantics need not exist,
but we are able to characterize the cases in which it exists and give
a decidable sufficient condition for the existence of the most specific concept.
Under this condition, it can be computed in polynomial time.
Franz Baader.
Least Common Subsumers and Most Specific Concepts in a Description Logic
with Existential Restrictions and Terminological Cycles.
In Georg Gottlob and Toby Walsh, editors, Proceedings of the 18th
International Joint Conference on Artificial Intelligence, pages
319–324. Morgan Kaufman, 2003.
Bibtex entry Paper (PDF)
Abstract
Computing least common subsumers (lcs) and most specific concepts (msc)
are inference tasks that can support the bottom-up construction
of knowledge bases in description logics.
In description logics with existential restrictions, the
most specific concept need not exist if one restricts the attention
to concept descriptions or acyclic TBoxes. In this paper,
we extend the notions lcs and msc to cyclic TBoxes. For
the description logic EL (which allows for conjunctions, existential
restrictions, and the top-concept), we show that the lcs and msc
always exist and can be computed in polynomial time if we
interpret cyclic definitions with greatest fixpoint semantics.
Franz Baader, editor.
Proceedings of the 19th International Conference on Automated Deduction
CADE-19, volume 2741 of Lecture Notes in Artificial
Intelligence.
Springer-Verlag, Miami Beach, FL, USA, 2003.
Bibtex entry
Franz Baader.
Restricted Role-value-maps in a Description Logic with Existential
Restrictions and Terminological Cycles.
In Proceedings of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.
Bibtex entry Paper (PDF)
Abstract
In a previous paper we have investigated subsumption in the presence of
terminological cycles for the description logic EL, which allows conjunctions,
existential restrictions, and the top concept, and have shown that the
subsumption problem remains polynomial for all three types of semantics usually
considered for cyclic de nitions in description logics. In this paper we show
that subsumption in EL (with or without cyclic de - nitions) remains polynomial
even if one adds a certain restricted form of global role-value-maps to EL. In
particular, this kind of role-value-maps can express transitivity of roles.
Franz Baader.
Terminological Cycles in a Description Logic with Existential
Restrictions.
In Georg Gottlob and Toby Walsh, editors, Proceedings of the 18th
International Joint Conference on Artificial Intelligence, pages
325–330. Morgan Kaufmann, 2003.
Bibtex entry Abstract
Abstract
Cyclic definitions in description logics have
until now been investigated only for description logics
allowing for value restrictions. Even for the most basic language
FL0, which allows for conjunction and value restrictions
only, deciding subsumption in the presence of terminological cycles
is a PSPACE-complete problem. This paper investigates subsumption
in the presence of terminological cycles for the language EL,
which allows for conjunction, existential restrictions, and the top-concept.
In contrast to the results for FL0, subsumption in
EL remains polynomial, independent of whether we use
least fixpoint semantics, greatest fixpoint semantics, or
descriptive semantics.
Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter F.
Patel-Schneider, editors.
The Description Logic Handbook: Theory, Implementation, and
Applications.
Cambridge University Press, 2003.
Bibtex entry Abstract
Abstract
Description Logics are a family of knowledge representation languages
that have been studied extensively in Artificial Intelligence over the
last two decades. They are embodied in several knowledge-based systems
and are used to develop various real-life applications. The Description
Logic Handbook provides a thorough account of the subject, covering all
aspects of research in this field, namely: theory, implementation, and
applications. Its appeal will be broad, ranging from more theoretically-oriented
readers, to those with more practically-oriented interests who need a sound
and modern understanding of knowledge representation systems based on
Description Logics. The chapters are written by some of the most prominent
researchers in the field, introducing the basic technical material before
taking the reader to the current state of the subject, and including
comprehensive guides to the literature. In sum, the book will serve as a
unique reference for the subject, and can also be used for self-study or
in conjunction with Knowledge Representation and Artificial Intelligence
courses.
Franz Baader, Jan Hladik, Carsten Lutz, and Frank Wolter.
From Tableaux to Automata for Description Logics.
Fundamenta Informaticae, 57:1–33, 2003.
Bibtex entry Paper (PS)
Abstract
This paper investigates the relationship between automata- and
tableau-based inference procedures for description logics. To be more
precise, we develop an abstract notion of what a tableau-based algorithm
is, and then show, on this abstract level, how tableau-based algorithms can
be converted into automata-based algorithms. In particular, this allows us
to characterize a large class of tableau-based algorithms that imply an
ExpTime upper-bound for reasoning in the description logics for which such
an algorithm exists.
Sebastian Brandt.
Implementing Matching in ALE—First Results.
In Proceedings of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
Matching problems in Description Logics are theoretically well understood,
with a variety of algorithms available for different DLs. Nevertheless, still
no implementation of a general matching algorithm exists. The present paper
presents an implementation of an existing matching algorithm for the DL
ALE and shows first results on benchmarks w.r.t. randomly generated
matching problems. The observed computation times show that the
implementation performs well even on relatively large matching problems.
Sebastian Brandt and Anni-Yasmin Turhan.
Computing least common subsumers for FLE^+.
In Proceedings of the 2003 International Workshop on Description
Logics, CEUR-WS, 2003.
Bibtex entry Paper (PS)
Abstract
Transitive roles are important for adequate representation of knowledge in a
range of applications. In this paper we present a first algorithm to compute
least common subsumers in a description logic with transitive roles.
Sebastian Brandt, Anni-Yasmin Turhan, and Ralf Küsters.
Extensions of Non-standard Inferences to Description Logics with transitive
Roles.
In Moshe Vardi and Andrei Voronkov, editors, Proceedings of the 10th
International Conference on Logic for Programming, Artificial Intelligence,
and Reasoning (LPAR 2003), Lecture Notes in Computer Science. Springer,
2003.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
Description Logics (DLs) are a family of knowledge representation
formalisms used for terminological reasoning. They have a wide range
of applications such as medical knowledge-bases, or the semantic
web. Research on DLs has been focused on the development of sound
and complete inference algorithms to decide satisfiability and
subsumption for increasingly expressive DLs.
Non-standard inferences are a group of relatively new inference
services which provide reasoning support for the building,
maintaining, and deployment of DL knowledge-bases. So far,
non-standard inferences are not available for very expressive DLs.
In this paper we present first results on non-standard inferences
for DLs with transitive roles. As a basis, we give a structural
characterization of subsumption for DLs where existential and value
restrictions can be imposed on transitive roles. We propose sound
and complete algorithms to compute the least common subsumer (lcs).
Nachum Dershowitz and Mitchell A. Harris.
Enumerating Satisfiable Propositional Formulae.
In Eurocomb, 2003.
Bibtex entry Paper (PDF)
Abstract
It is known experimentally that there is a threshold for
satisfiability in 3-CNF formulas around the value 4.25 for the
ratio of variables to clauses. It is also known that the threshold
is sharp, but that proof does not give a value for the
threshold.
We use purely combinatorial techniques to count the number of
satisfiable boolean formulas given in conjunctive normal form.
The intention is to provide information about the relative
frequency of boolean functions with respect to statements of a
given size, and to give a closed form formula for any number of
variables, literals and clauses. We describe a correspondence
between the syntax of propositions to the semantics of functions
using a system of equations and show how to solve such a system.
J. Hladik and U. Sattler.
A Translation of Looping Alternating Automata to Description Logics.
In Proc. of the 19th Conference on Automated Deduction (CADE-19),
volume 2741 of Lecture Notes in Artificial Intelligence. Springer
Verlag, 2003.
Bibtex entry Paper (PS) ©Springer-Verlag
Jan Hladik.
Reasoning about Nominals with FaCT and RACER.
In Proceedings of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.
Bibtex entry Paper (PS)
Abstract
We present a translation of looping alternating two-way automata into a
comparably inexpressive description logic, which is contained in SHIQ. This
enables us to perform the emptiness test for a language accepted by such an
automaton using the systems FaCT and RACER. We implemented our translation
and performed a test using automata which accept models for ALCIO concepts,
so that we can use SHIQ systems to reason about nominals. Our empirical
results show, however, that the resulting knowledge bases are hard to
process for both systems.
I. Horrocks and U. Sattler.
Decidability of SHIQ with Complex Role Inclusion Axioms.
In Proc. of the International Joint Conference on Artificial Intelligence (IJCAI-2003). Morgan-Kaufmann Publishers, 2003.
Bibtex entry Paper (PDF)
O. Kutz, C. Lutz, F. Wolter, and M. Zakharyaschev.
E-connections of Description Logics.
In Proceedings of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.
Bibtex entry Paper (PS)
Abstract
Recently, E-connections have been proposed as a new means for
connecting knowledge representation systems. We illustrate how this
connection technique can be used for combining description logics,
thereby surveying various extensions of the original E-connections.
For all these extensions, general transfer results for concept
satisfiability are given.
C. Lutz.
Description Logics with Concrete Domains—A Survey.
In Advances in Modal Logics Volume 4. World Scientific Publishing Co. Pte. Ltd., 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, C. Areces, I. Horrocks, and U. Sattler.
Keys, Nominals, and Concrete Domains.
In Proceedings of the Eighteenth International Joint Conference on
Artificial Intelligence IJCAI-03, Acapulco, Mexico, 2003.
Morgan-Kaufmann Publishers.
Bibtex entry Paper (PS)
Abstract
Many description logics (DLs) combine knowledge representation on an
abstract, logical level with an interface to "concrete" domains
such as numbers and strings. We propose to extend such DLs with key
constraints that allow the expression of statements like "US citizens are
uniquely identified by their social security number". Based on this
idea, we introduce a number of natural description logics and
present (un)decidability results and tight NExpTime complexity bounds.
C. Lutz, U. Sattler, and L. Tendera.
The Complexity of Finite Model Reasoning in Description Logics.
In Proc. of the 19th Conference on Automated Deduction (CADE-19),
volume 2741 of Lecture Notes in Artificial Intelligence. Springer
Verlag, 2003.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
We analyze the complexity of finite model reasoning in the
description logic ALCQI, i.e. ALC augmented with qualifying
number restrictions, inverse roles, and general TBoxes. It turns out
that all relevant reasoning tasks such as concept satisfiability and
ABox consistency are ExpTime-complete, regardless of whether
the numbers in number restrictions are coded unarily or binarily.
Thus, finite model reasoning with ALCQI is not harder than standard
reasoning with ALCQI.
C. Lutz, U.Sattler, and L. Tendera.
Finite Model reasoning in ALCQI is ExpTime-complete.
In Proceedings of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.
Bibtex entry Paper (PS)
Abstract
We analyze the complexity of finite model reasoning in the
description logic ALCQI, i.e.ALC augmented with qualifying
number restrictions, inverse roles, and general TBoxes. It turns out
that all relevant reasoning tasks such as concept satisfiability and
ABox consistency are ExpTime-complete, regardless of whether
the numbers in number restrictions are coded unarily or binarily.
Thus, finite model reasoning with ALCQI is not harder than standard
reasoning with ALCQI.
C. Lutz, F. Wolter, and M. Zakharyaschev.
Reasoning about concepts and similarity.
In Proceedings of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.
Bibtex entry Paper (PS)
Abstract
In many application areas, there exist concepts that are too vague to be
captured by classical DL concept definitions. Based on this observation,
we combine the description logic ALCQO with the logic MS for reasoning
about metric spaces, and propose to use the resulting "hybrid" for the
definition of concepts based on similarity measures: concepts can be
defined by referring to (the similarity to) proptypical instances. We
sketch a tableau algorithm for our logic and present an undecidability
result illustrating that it can be dangerous to allow a too close
interaction between the DL and MS.
C. Lutz, F. Wolter, and M. Zakharyaschev.
A tableau algorithm for reasoning about concepts and similarity.
In Proceedings of the Twelfth International Conference on Automated
Reasoning with Analytic Tableaux and Related Methods TABLEAUX 2003,
LNAI, Rome,Italy, 2003. Springer.
Bibtex entry Paper (PS) ©Springer-Verlag
Abstract
We present a tableau-based decision procedure for the fusion
(independent join) of the expressive description logic
ALCQO and the logic MS for reasoning about
distances and similarities. The resulting "hybrid" logic allows
both precise and approximate representation of and reasoning about
concepts. The tableau algorithm combines the existing tableaux for
the components and shows that the tableau technique can be
fruitfully applied to fusions of logics with nominals-the case in
which no general decidability transfer results for fusions are
available.
U. Sattler.
Description Logics for Ontologies.
In Proc. of the International Conference on Conceptual Structures (ICCS
2003), volume 2746 of LNAI. Springer Verlag, 2003.
Bibtex entry Paper (PS) ©Springer-Verlag
U. Sattler, D. Calvanese, and R. Molitor.
Relationship with other Formalisms.
In Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and
Peter F. Patel-Schneider, editors, The Description Logic Handbook:
Theory, Implementation, and Applications, pages 137–177. Cambridge
University Press, 2003.
Bibtex entry Abstract
Abstract
In this chapter, we are concerned with the relationship between description
logics and other formalisms, regardless of whether they were designed for
knowledge representation issues or not. Obviously, due to the lack of space,
we cannot compare each representational formalism with DLs, thus we
concentrated on those that either (1) had or have a strong influence on DLs
(e.g., modal logics), (2) are closely related to description logics for
historical reasons (e.g., semantic networks and structured inheritance
networks), (3) have similar expressive power (e.g., semantic data models).
Back to the homepage of the Chair for Automata Theory.
Generated at Sat Feb 4 10:56:31 CET 2012.