Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Publications
1998
C.A. Albayrak.
Die WHILE-Hierarchie für Programmschemata.
PhD thesis, RWTH Aachen, 1998.
Bibtex entry
Can Adam Albayrak and Thomas Noll.
The WHILE Hierarchy of Program Schemes is Infinite.
In Maurice Nivat, editor, Proceedings of Foundations of Software Science
and Computation Structures, pages 35–47. LNCS 1378, Springer, 1998.
Bibtex entry
F. Baader.
On the Complexity of Boolean Unification.
Information Processing Letters, 67(4):215–220, 1998.
Bibtex entry Abstract
Abstract
Unification modulo the theory of Boolean algebras has been investigated
by several autors. Nevertheless, the exact complexity of the decision problem
for unification with constants and general unification was not
known. In this research note, we show that the decision problem is
$\Pi^p_2$-complete for unification with constants and
PSPACE-complete for general unification. In contrast, the decision
problem for elementary unification (where the terms to be unified
contain only symbols of the signature of Boolean algebras) is
``only'' NP-complete.
F. Baader, A. Borgida, and D.L. McGuinness.
Matching in Description Logics: Preliminary Results.
In M.-L. Mugnier and M. Chein, editors, Proceedings of the Sixth
International Conference on Conceptual Structures (ICCS-98), volume 1453
of Lecture Notes in Computer Science, pages 15–34, Montpelier (France), 1998. Springer–Verlag.
Bibtex entry Abstract
Abstract
Matching of concepts with variables (concept patterns)
is a relatively new operation that has been introduced
in the context of concept description languages (description
logics), originally to help filter out unimportant aspects
of large concepts appearing in industrial-strength knowledge
bases. This paper proposes a new approach to performing matching,
based on a ``concept-centered'' normal form, rather than the more
standard ``structural subsumption'' normal form for concepts. As
a result, matching can be performed (in polynomial time) using
arbitrary concept patterns of a description language allowing for
conjunction, value restriction, and atomic negation, thus removing
restrictions on the form of the patterns from previous work. The
paper also addresses the question of matching problems with
additional ``side conditions'', which were motivated by practical
experience.
F. Baader and R. Küsters.
Computing the least common subsumer and the most specific concept in the
presence of cyclic ALN-concept descriptions.
In O. Herzog and A. Günter, editors, Proceedings of the 22nd Annual
German Conference on Artificial Intelligence, KI-98, volume 1504 of
Lecture Notes in Computer Science, pages 129–140, Bremen, Germany, 1998.
Springer–Verlag.
Bibtex entry Abstract
Abstract
Computing least common subsumers (lcs) and most specific concepts (msc)
are inference tasks that can be used to support the ``bottom up''
construction of knowledge bases for KR systems based on description
logic. For the description logic ALN, the msc
need not always exist if one restricts the attention to acyclic
concept descriptions. In this paper, we extend the notions lcs and msc
to cyclic descriptions, and show how they can be computed.
Our approach is based on the automata-theoretic characterizations of
fixed-point semantics for cyclic terminologies developed in previous
papers.
F. Baader and R. Küsters.
Least common subsumer computation w.r.t. cyclic
ALN-terminologies.
In Proceedings of the 1998 International Workshop on Description Logics (DL'98), Trento, Italy, 1998.
Bibtex entry Paper (PS)
Abstract
Computing least common subsumers (lcs) and most specific concepts (msc)
are inference tasks that can be used to support the ``bottom up''
construction of knowledge bases for KR systems based on description
logic. For the description logic $\mathcal{ALN}$, the msc
need not always exist if one restricts the attention to acyclic
concept descriptions. In this paper, we extend the notions lcs and msc
to cyclic descriptions, and show how they can be computed.
Our approach is based on the automata-theoretic characterizations of
fixed-point semantics for cyclic terminologies developed in previous
papers.
F. Baader, R. Küsters, and R. Molitor.
Structural Subsumption Considered from an Automata Theoretic Point of
View.
In Proceedings of the 1998 International Workshop on Description Logics
DL'98, Trento, Italy, 1998.
Bibtex entry Paper (PS)
Abstract
This paper compares two approaches for deriving subsumption algorithms for the
description logic ALN: structural subsumption and an automata-theoretic
characterization of subsumption. It turns out that structural subsumption
algorithms can be seen as special implementations of the automata-theoretic
characterization.
F. Baader and P. Narendran.
Unification of Concept Terms in Description Logics.
In H. Prade, editor, Proceedings of the 13th European Conference on
Artificial Intelligence (ECAI-98), pages 331–335. John Wiley & Sons
Ltd, 1998.
Bibtex entry Abstract
Abstract
Unification of concept terms is a new kind of inference problem
for Description Logics, which extends the equivalence problem by
allowing to replace certain concept names by concept terms
before testing for equivalence. We show that this inference problem
is of interest for applications, and present first decidability
and complexity results for a small concept description language.
F. Baader and U. Sattler.
Description Logics with Concrete Domains and Aggregation.
In H. Prade, editor, Proceedings of the 13th European Conference on
Artificial Intelligence (ECAI-98), pages 336–340. John Wiley & Sons
Ltd, 1998.
Bibtex entry Paper (PS)
F. Baader and K. Schulz.
Combination of Constraint Solvers for Free and Quasi-Free Structures.
Theoretical Computer Science, 192:107–161, 1998.
Bibtex entry Free reprint
Abstract
When combining languages for symbolic constraints, one is
typically faced with the
problem of how to treat ``mixed'' constraints. The two main problems
are (1) how to define a combined solution structure over which these
constraints are to be solved, and (2) how to combine the constraint solving
methods for pure constraints into one for mixed constraints.
The paper introduces the notion of a ``free amalgamated product'' as a possible solution
to the first problem. We define so-called quasi-free structures
(called ``strong simply-combinable structures'' in a previous publication) as
a generalization of free structures.
For quasi-free structures over disjoint signatures, we describe
a canonical amalgamation construction that yields the free amalgamated product.
The combination techniques known from unification theory
can be used to combine constraint solvers for quasi-free structures over disjoint
signatures into a solver for their free amalgamated product.
In addition to term algebras modulo equational theories (i.e., free algebras),
the class of quasi-free structures
contains many solution structures that are of interest in constraint logic programming,
such as the algebra of rational trees, feature
structures, and domains consisting of hereditarily finite
(wellfounded or non-wellfounded) nested sets and lists.
F. Baader and K.U. Schulz.
Unification Theory.
In W. Bibel and P.H. Schmidt, editors, Automated Deduction – A Basis for
Applications, Vol. I: Foundations – Calculi and Methods, volume 8 of
Applied Logic Series, pages 225–263. Kluwer Academic Publishers,
Dordrecht, NL, 1998.
Bibtex entry Abstract
Abstract
In this chapter, we first motivate equational unification by
its applications in theorem proving and term rewriting. In addition
to applications that require the computation of unifiers, we will also
mention constraint-based approaches, in which only solvability of unification
problems (i.e., the existence of unifiers) must be tested.
Then we extend the definitions known from syntactic unification (such as most
general unifier) to the case of equational unification. It turns out that, for
equational unification, one must be more careful when introducing these
notions. In the third section, we will mention some unification results
for specific equational theories. In the fourth, and central, section of this
chapter, we treat the important problem of how to combine unification
algorithms. This problem occurs, for example, if we have a
unification algorithm that can treat the commutative symbol ``+''
and another algorithm that can treat the associative symbol ``x'',
and we want to unify terms that contain both symbols.
Finally, we conclude with a short section in which other interesting
topics in the field of equational unification are mentioned,
which could not be treated in more detail in this chapter.
F. Baader and C. Tinelli.
Deciding the Word Problem in the Union of Equational Theories.
UIUCDCS-Report UIUCDCS-R-98-2073, Department of Computer Science, University
of Illinois at Urbana-Champaign, 1998.
Bibtex entry Paper (PS)
Abstract
The main contribution of this report 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.''
In addition, we show that---contrary to a common belief---the Nelson-Oppen
combination method cannot be used to combine decision procedures
for the word problem, even in the case of equational theories with
disjoint signatures.
Franz Baader and Tobias Nipkow.
Term Rewriting and All That.
Cambridge University Press, United Kingdom, 1998.
Bibtex entry Abstract
Abstract
This is the first English language textbook offering a unified and
self-contained introduction to the field of term rewriting. It covers all the
basic material (abstract reduction systems, termination, confluence, completion,
and combination problems), but also some important and closely connected
subjects: universal algebra, unification theory and Gröbner bases. The main
algorithms are presented both informally and as programs in the functional
language Standard ML (an appendix contains a quick and easy introduction to
ML). Certain crucial algorithms like unification and congruence closure are
covered in more depth and efficient Pascal programs are developed. The book
contains many examples and over 170 exercises.
This text is also an ideal reference book for professional researchers: results
that have been spread over many conference and journal articles are collected
together in a unified notation, detailed proofs of almost all theorems are
provided, and each chapter closes with a guide to the literature.
More
Information (Table of contents, sample programs, errata)
Cyril Decleir, Mohand-Said Hacid, and Jacques Kouloumdjian.
Modeling and Querying Video Data: A Hybrid Approach.
In Proceedings of the IEEE Workshop on Content-Based Access of Image &
Video Libraries (CBAIVL'98), Santa Barbara, CA, USA, pages 86–90. IEEE
Computer Society, June 1998.
Bibtex entry Paper (PS)
Abstract
This paper develops a video data model and a rule-based query language
for video retrieval. A video sequence is split into a set of fragments.
Each fragment can be analyzed to extract the information of interest that can
be put into a database. This database can then be searched to find information
of interest. Two types of information are considered: (1) the entities (i.e., objects)
of interest in a video sequence, (2) generalized strata (a set of fragments), which
contain these entities. To represent these information, our data model allows
facts as well as objects and constraints. We present a declarative, rule-based,
constraint query language that can be used to infer relationships about
information represented in the model. The language has a clear declarative
and operational semantics.
Cyril Decleir, Mohand-Said Hacid, and Jacques Kouloumdjian.
Modeling and Querying Video Databases.
In Proceedings 24th EUROMICRO'98 Conference Workshop on Multimedia and
Telecommunications, Vasteras, Sweden, pages 492–498. IEEE Computer
Society, August 1998.
Bibtex entry Paper (PS)
Abstract
Indexing video data is essential for providing content based access.
This paper develops a data model and a rule-based query language
for video content based indexing and retrieval. The data model is based
on the notion of generalized strata, which can be seen as a set
of intervals. Each interval can be analyzed to extract symbolic
descriptions of interest that can be put into a database.
This database can then be searched to find information
of interest. Two types of information are considered: (1) the entities (i.e., objects)
in the domain of a video sequence, (2) video frames, called
generalized strata, which contain these entities. To represent these information, our
data model allows
facts as well as objects and constraints. We present a declarative, rule-based,
constraint query language that can be used to infer relationships about
information represented in the model. In the video application
we are interested in, we wish to construct new generalized strata from old
ones. To do this, our language has an interpreted function term (i.e., constructive term)
to concatenate generalized strata. This language has a clear declarative
and operational semantics.
H.-W. Denker, J. Hiltner, H.-P. Hohn, D. C. Novak, B. Reusch, C. Tresp, and
J. Weidemann.
Schnittbildanatomie – Interaktives klinisch-topographisches
Lernprogramm.
W. de Gruyter, 1998.
Bibtex entry
I. Horrocks and U. Sattler.
A Description Logic with Transitive and Converse Roles and Role
Hierarchies.
In Proceedings of the International Workshop on Description Logics,
Povo - Trento, Italy, 1998. IRST.
Bibtex entry Paper (PS)
R. Küsters.
Characterizing the Semantics of Terminological Cycles in
ALN using Finite Automata.
In Proceedings of the Sixth International Conference on Principles of
Knowledge Representation and Reasoning (KR'98), pages 499–510. Morgan
Kaufmann, 1998.
Bibtex entry Abstract
Abstract
The representation of terminological knowledge may naturally lead to terminological cycles. In
addition to descriptive semantics, the meaning of cyclic terminologies can
also be captured by fixed-point semantics, namely, greatest and least
fixed-point semantics. To gain a more profound understanding
of these semantics and to obtain inference algorithms as well as complexity
results for inconsistency, subsumption, and
related inference tasks, this paper provides automata theoretic
characterizations of these semantics. More precisely,
the already existing results for \flnull{} are extended to the language \aln{}, which
additionally allows for primitive negation and number-restric\-tions.
Unlike \flnull, the language \aln{} allows to express inconsistent concepts, which
makes non-trivial extensions of the characterizations and algorithms
necessary. Nevertheless, the complexity of reasoning does not increase when
going from \flnull{} to \aln{}. This distinguishes \aln{} from the very
expressive languages with fixed-point operators proposed in the literature. It
will be shown, however, that cyclic \aln{}-terminologies are expressive enough to capture
schemas in certain semantic data models.
Martin Leucker and Stephan Tobies.
Truth—A Platform for Verification of Distributed Systems.
Aachener Informatik Bericht 98-05, RWTH Aachen, May 1998.
Bibtex entry Paper (PS)
Abstract
Formal Methods are becoming more an more important for the development of
hardware and software systems. Verification tools support the employment of
Formal Methods. This paper gives an overview of the design and implementation of
the verification tool Truth. We define and explain requirements for verification
tools. Furthermore, we discuss several semantic models, specification languages
and logics and their visualisation from a tool builder's perspective and show
how these requirements were adopted in Truth.",
U. Sattler.
Terminological knowledge representation systems in a process engineering
application.
PhD thesis, LuFG Theoretical Computer Science, RWTH-Aachen, 1998.
Bibtex entry Paper (PS)
Abstract
This work is concerned with the question of how far terminological knowledge
representation systems can support the development of mathematical models of
chemical processes. Terminological knowledge representation systems are based on
Description Logics, a highly expressive formalism with well-defined semantics,
and provide powerful inference services. These system services can be used to
support the structuring of the application domain, namely the organised storage
of parts of process models. However, the process systems engineering
application asks for the extension of the expressive power of already existing
Description Logics, particularly with transitive roles and expressive number
restrictions. These extensions are introduced and investigated with respect to
the computational complexity of the corresponding inference problems.
Stephan Tobies.
Design und Implementierung einer Plattform zur Verifikation verteilter
Systeme.
Diploma thesis, RWTH Aachen, Germany, 1998.
Bibtex entry Paper (PS)
Abstract
Formal Methods are becoming more an more important for the development of
hardware and software systems. Verification tools support the employment of
Formal Methods. This thesis gives an overview of the design and implementation of
the verification tool Truth.
C. Tresp and U. Tüben.
Medical Terminology Processing for a Tutoring System.
In International Conference on Computational Intelligence and Multimedia
Applications (ICCIMA98), Monash Univ. (Australien), Februar 1998.
Bibtex entry
C.B. Tresp and R. Molitor.
A Description Logic for Vague Knowledge.
In Proceedings of the 13th biennial European Conference on Artificial
Intelligence (ECAI'98), pages 361–365, Brighton, UK, 1998. J. Wiley and
Sons.
Bibtex entry Abstract
Abstract
This work introduces the concept language ALC F(M), which is an extension of ALC
to many-valued logics. ALC F(M) allows to express vague concepts, e.g. more or
less enlarged or very small.
To realize this extension to many-valued logics, the classical notions of
satisfiability and subsumption had to be modified appropriately. The main
contribution of this paper is a sound and complete method for computing the
degree of subsumption between two ALC F(M)-concepts.
Back to the homepage of the Chair for Automata Theory.
Generated at Mon Apr 30 13:36:07 CEST 2012.