Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Publications
1996
F. Baader.
Combination of Compatible Reduction Orderings that are Total on Ground
Terms.
In Proceedings of the 10th International Workshop on Unification,
UNIF-96, CIS-Report 96-91, pages 97–106. CIS, Universität München,
1996.
Bibtex entry Paper (PS)
Abstract
Reduction orderings that are compatible with an equational theory $E$ and total
on the $E$-equivalence classes of ground terms play an important role in automated
deduction. It has turned out to be rather hard to define such orderings.
This paper supports the process of designing compatible total reduction orderings.
It describes how total reduction orderings $>_1$ and $>_2$ that are respectively
compatible with $E_1$ and $E_2$ can be combined to a total reduction ordering $>$ that is
compatible with $E_1 \cup E_2$, provided that the theories are over disjoint signatures
and some other properties are satisfied.
F. Baader.
A Formal Definition for the Expressive Power of Terminological Knowledge
Representation Languages.
J. of Logic and Computation, 6(1):33–54, 1996.
Bibtex entry Free reprint
Abstract
The notions `expressive power' or `expressiveness' of knowledge
representation languages (KR languages) can be found in most papers
on knowledge representation; but these terms are usually just
employed in an intuitive sense. The papers contain only informal
descriptions of what is meant by expressiveness. There are several
reasons that speak in favour of a formal definition of
expressiveness: for example, if we want to show that certain
expressions in one language cannot be expressed in another
language, we need a strict formalism that can be used in
mathematical proofs.
Even though we shall only consider terminological KR
languages---i.e. KR languages descending from the original system
KL-ONE---in our motivation and in the examples, the definition of
expressive power that will be given in this paper can be used for
all KR languages with Tarski-style model-theoretic semantics. This
definition will shed a new light on the tradeoff between
expressiveness of a representation language and its computational
tractability. There are KR languages with identical expressive
power, but different complexity results for reasoning, which comes
from the fact that sometimes the tradeoff lies between convenience
and computational tractability. The definition of expressive power
will be applied to compare various terminological KR languages known
from the literature with respect to their expressiveness. This will
yield examples for how to utilize the definition both in positive
proofs---that is, proofs where it is shown that one language can be
expressed by another language---and, more interestingly, in negative
proofs---which show that a given language cannot be expressed by the
other language.
F. Baader.
Logik-basierte Wissensrepräsentation.
KI, 3/96:8–16, 1996.
Bibtex entry Abstract
Abstract
Nach einer kurzen Betrachtung der Anforderungen, die eine
Wissensrepr"asentationssprache erf"ullen sollte, werden wir
auf Beschreibungslogiken, Modallogiken und nichtmonotone Logiken
als Formalismen zur Repr"asentation terminologischen Wissens,
zeitabh"angigen und subjektiven Wissens sowie unvollst"andigen Wissens
eingehen. Am Ende jedes Abschnitts wird kurz auf die Verbindung zur Logischen
Programmierung eingegangen.
F. Baader.
Using Automata Theory for Characterizing the Semantics of Terminological
Cycles.
Annals of Mathematics and Artificial Intelligence, 18(2–4):175–219,
1996.
Bibtex entry Free reprint
Abstract
In most of the implemented terminological knowledge representation systems it is
not possible to state recursive concept definitions, so-called terminological
cycles. One reason is that it is not clear what kind of semantics to use for
such cyles. In addition, the inference algorithms used in such systems may go
astray in the presence of terminological cycles. In this paper we consider
terminological cycles in a very small terminological representation language.
For this language, the effect of the three types of semantics introduced by B.
Nebel can completely be described with the help of finite automata. These
descriptions provide for a rather intuitive understanding of terminologies with
recursive definitions, and they give an insight into the essential features of
the respective semantics. In addition, one obtains algorithms and complexity
results for the subsumption problem and for related inference tasks. The results
of this paper may help to decide what kind of semantics is most appropriate for
cyclic definitions, depending on the representation task.
F. Baader, M. Buchheit, and B. Hollunder.
Cardinality Restrictions on Concepts.
Artificial Intelligence, 88(1–2):195–213, 1996.
Bibtex entry Free reprint
Abstract
The concept description formalisms of existing description logics
systems allow the user to express local cardinality restrictions on
the fillers of a particular role. It is not possible, however, to
introduce global restrictions on the number of instances of a given
concept. This article argues that such cardinality restrictions on
concepts are of importance in applications such as configuration of
technical systems, an application domain of description logics
systems that is currently gaining in interest. It shows that
including such restrictions in the description language leaves the
important inference problems such as instance testing decidable.
The algorithm combines and simplifies the ideas developed for the
treatment of qualified number restrictions and of general
terminological axioms.
F. Baader and W. Nutt.
Combination Problems for Commutative/Monoidal Theories: How Algebra Can
Help in Equational Reasoning.
J. Applicable Algebra in Engineering, Communication and Computing,
7(4):309–337, 1996.
Bibtex entry Abstract
Abstract
We study the class of theories for which solving unification
problems is equivalent to solving systems of linear equations
over a semiring. It encompasses important examples like the theories of
Abelian monoids, idempotent Abelian monoids, and Abelian groups.
This class has been introduced by the authors independently
of each other as ``commutative theories'' (Baader)
and ``monoidal theories'' (Nutt).
We show that commutative theories and monoidal theories indeed define the same class
(modulo a translation of the signature), and we prove that it is undecidable
whether a given theory belongs to it.
In the remainder of the paper we investigate
combinations of commutative/monoidal theories with other theories.
We show that finitary commutative/monoidal theories always satisfy the
requirements for applying general methods developed for the combination of
unification algorithms for disjoint equational theories.
Then we study the adjunction of monoids of homomorphismss to
commutative/monoidal theories.
This is a special case of a non-disjoint combination,
which has an algebraic counterpart in the corresponding semiring.
By studying equations over this semiring,
we identify a large subclass of commutative/monoidal theories
that are of unification type zero by.
We also show with methods from linear algebra
that unitary and finitary commutative/monoidal theories
do not change their unification type
when they are augmented by a finite monoid of \hom s,
and how algorithms for the extended theory can be obtained from
algorithms for the basic theory.
F. Baader and U. Sattler.
Description Logics with Symbolic Number Restrictions.
In W. Wahlster, editor, Proceedings of the Twelfth European Conference on
Artificial Intelligence (ECAI-96), pages 283–287. John Wiley & Sons
Ltd, 1996.
An extended version has appeared as Technical Report LTCS-96-03.
Bibtex entry Paper (PS)
Abstract
Motivated by a chemical engineering application,
we introduce an extension of the concept description language ALCN by
symbolic number restrictions. This first extension turns out to have an
undecidable concept satisfiability problem. For a restricted language-whose
expressive power is sufficient for our application-we show that concept
satisfiability is decidable.
F. Baader and U. Sattler.
Knowledge Representation in Process Engineering.
In Proceedings of the International Workshop on Description Logics,
Cambridge (Boston), MA, U.S.A., 1996. AAAI Press/The MIT Press.
Bibtex entry Paper (PS)
Abstract
In process engineering, as in many other application domains, the domain
specific knowledge is far too complex to be described entirely using description
logics. Hence this knowledge is often stored using an object-oriented system,
which, because of its high expressiveness, provides only weak inference
services. In particular, the process engineers at RWTH Aachen have developed a
frame-like language for describing process models. In this paper, we investigate
how the powerful inference services provided by a DL system can support the
users of this frame-based system. In addition, we consider extensions of
description languages that are necessary to represent the relevant process
engineering knowledge.
F. Baader and U. Sattler.
Number Restrictions on Complex Roles in Description Logics.
In Proceedings of the Fifth International Conference on the Principles of
Knowledge Representation and Reasoning (KR-96). Morgan Kaufmann, Los
Altos, 1996.
An extended version has appeared as Technical Report LTCS-96-02.
Bibtex entry Abstract
Abstract
Number restrictions are concept constructors that are available in
almost all implemented description logic systems. However,
even though there has lately been considerable effort on integrating
expressive role constructors into description logics, the roles
that may occur in number restrictions are usually of a very
restricted type. Until now, only languages with number
restrictions on atomic roles and inversion of atomic roles, or
with number restrictions on intersection of
atomic roles have been investigated in detail.
In the present paper, we increase the expressive power of description languages
by allowing for more complex roles in number restrictions. As role constructors,
we consider composition of roles (which will be present in all our languages),
and intersection, union and inversion of roles in different combinations. We
will present one decidability result (for the basic language that extends ALC
by number restrictions on roles with composition), and three undecidability
results for three different extensions of the basic language.
F. Baader and K. U. Schulz.
Unification in the Union of Disjoint Equational Theories: Combining
Decision Procedures.
J. Symbolic Computation, 21:211–243, 1996.
Bibtex entry Free reprint
Abstract
Most of the work on the combination of unification algorithms for the
union of disjoint equational theories has been restricted to algorithms
that compute finite complete sets of unifiers. Thus the developed combination
methods usually cannot be used to combine decision procedures, i.e.,
algorithms that just decide solvability of unification problems without
computing unifiers.
In this paper we describe a combination algorithm for decision procedures
that works for arbitrary equational theories, provided that solvability of
so-called unification problems with constant restrictions---a slight
generalization of unification problems with constants---is decidable for
these theories.
As a consequence of this new method, we can, for example, show that general
A-unifiability, i.e., solvability of A-unification problems with free
function symbols, is decidable. Here A stands for the equational theory of
one associative function symbol.
Our method can also be used to combine algorithms that compute finite
complete sets of unifiers. Manfred Schmidt-Schau{\ss}' combination result,
the until now most general result in this direction, can be obtained as a
consequence of this fact.
We also obtain the new result that unification in the union of disjoint
equational theories is finitary, if general unification---i.e., unification
of terms with additional free function symbols---is finitary in the single
theories.
Franz Baader and Klaus U. Schulz, editors.
Frontiers of Combining Systems.
Proceedings of First International Workshop, Applied Logic Series 3. Kluwer
Academic Publishers, 1996.
Bibtex entry Abstract
Abstract
The combination of formal systems and algorithms, the logical
and algebraic background, as well as the general architecture
of complex and interacting systems has recently become a very
active research area. The first international workshop
Frontiers of Combining Systems created a common forum for the
different research activities on this topic in the fields of
logic, computer science, and artificial intelligence. Its main
intention was to stimulate an interdisciplinary discussion that
focuses on different aspects of the combination problem.
The volume contains research papers that cover the combination
of logics, the combination of constraint-solving techniques and
decision procedures, the combination of deductive systems, the
integration of data structures into Constraint Logic
Programming formalisms, and logic modelling of multi-agent
systems. These problems are addressed on different conceptual
levels: from the investigation of formal properties of combined
systems using methods of logic and mathematics to the
consideration of physical connections and communication
languages relavent for combination of software tools.
Table of Contents
Kamel Ben-Khalifa.
Kombination freier Strukturen.
Diploma thesis, RWTH Aachen, Germany, November 1996.
Bibtex entry Paper (PS)
Abstract
Bei dem Kombinationsproblem in der Unifikationstheorie geht es darum,
Unifikationsalgorithmen für Gleichungstheorien über disjunkten Signaturen zu
einem Unifikationsalgorithmus zu kombinieren, der Unifikationsprobleme über der
gemischten Signatur, d.h. Unifikationsprobleme in denen Symbole aus
verschiedenen Gleichungstheorien vorkommen können, behandeln kann. Eine
Erweiterung dieses Problems besteht darin, Termrelationen zu betrachten, die
allgemeiner sind, als die Gleichheit modulo einer Gleichungstheorie. Die Klasse
der Knuth-Bendix Reduktionsordnungen, die z.B. bei der Vervollständigung von
Termersetzungssystemen Verwendung findet, ist ein wichtiges Beispiel solcher
Termrelationen.
Dazu muß man aber zuerst festlegen, wie diese Relationen auf den gemischten
Termen zu interpretieren sind. Dazu existieren zwei Definitionen. Die
Definition von Baader und Schulz ist eine algebraische Definition, die auf einer
geeigneten Kombination von freien Strukturen basiert. Die Definition von
Kirchner und Ringeissen ist hingegen syntaktisch. Sie verwendet Termreduktion und
Termabstraktion. In dieser Arbeit wird im wesentlichen gezeigt, daß beide
Definitionen äquivalent sind. Anschließend wird gezeigt, wie man ausgehend von
einer Modifikation der syntaktischen Definition Entscheidungsverfahren für die
Gültigkeit von reinen atomaren Formeln zu einem Entscheidungsverfahren für die
Gültigkeit von atomaren Formeln über der gemischten Signatur kombinieren kann.
J. Hiltner and C. Tresp.
Verbunddokumente: Objektmodelle und Implementierungen.
In 15. Workshop Interdisziplinäre Methoden in der Informatik,
Forschungsberichte der Universität Dortmund, 1996.
Bibtex entry
Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith,
Jörn Richts, and Jörg Siekmann.
Die Beweisentwicklungsumgebung Omega-MKRP.
Informatik – Forschung und Entwicklung, 11(1):20–26, 1996.
In German.
Bibtex entry Paper (PS)
Abstract
The main goal of the proof development environment Omega-MKRP is to support
mathematicians in one of their main activities, namely proving mathematical
theorems. This support must be so comfortable that formal proofs can be
generated without undue difficulties and the correctness of the generated proofs
is ensured. Such a system will only succeed if the computer supported generation
of proofs is less time consuming than manual generation. In order to achieve
this, there are different requirements to be fulfilled, which we describe in
this paper. In particular, we discuss the expressive power of the object
language, the possibility to communicate abstract proof plans, the automated
support in filling proof gaps, and the human-oriented presentation of proofs
generated. Omega-MKRP is a synthesis of the approaches of fully automated,
interactive, and plan-based theorem proving. This article gives a survey of
various aspects of the system.
Martin Leucker.
Comparison of Two Semantic Approaches to Unification.
Diploma thesis, RWTH Aachen, Germany, 1996.
In German.
Bibtex entry Paper (PS)
Abstract
This thesis compares the two most prominent semantic approaches to unification
in equational theories.
We can show that unification in primal algebras is not a direct instance
of unification in monoidal theories. However, it is possible to reduce
unification in a given primal algebra to unification in a corresponding monoidal
theory. As by-products of this work we have shown that unification in algebras
is an instance of unification modulo equational theories, and we have introduced
a new notion of equivalence for equational theories.
E. Meyer zu Bexten, C. Tresp, M. Jäger, M. Moser, and J. Hiltner.
Consistency Checking in Applications based on Fuzzy Rules.
In Second International Conference on Applications of Fuzzy Systems and
Soft Computing, Siegen (Deutschland), Juni 1996.
Bibtex entry
U. Sattler.
A Concept Language Extended with Different Kinds of Transitive Roles.
In G. Görz and S. Hölldobler, editors, 20. Deutsche Jahrestagung
für Künstliche Intelligenz, number 1137 in Lecture Notes in
Artificial Intelligence. Springer Verlag, 1996.
Bibtex entry Paper (PS)
Abstract
Motivated by applications that demand for the adequate representation of
part-whole relations, different possibilities of representing transitive
relations in terminological knowledge representation systems are investigated.
A well-known concept language, ALC, is extended by three different kinds of
transitive roles. It turns out that these extensions differ largely in
expressiveness and computational complexity, hence this investigation gives
insight into the diverse alternatives for the representation of transitive
relations such as part-whole relations, family relations or partial orders in
general.
U. Sattler.
Knowledge Representation in Process Engineering.
In F. Baader, H. J. Bürckert, A. Günter, and W. Nutt, editors,
Proceedings of the Workshop on Knowledge Representation and Configuration (WRKP'96), DFKI Document D-96-04. Deutsches Forschungszentrum für
Künstliche Intelligenz GmbH, 1996.
Bibtex entry Paper (PS)
K. Tochtermann, C. Tresp, J. Hiltner, and A. Freund.
HyperMed: A Hypermedia System for Anatomical Education.
In ED-Media, World Conference on Educational Multimedia and Hypermedia,
Boston (USA), August 1996.
Bibtex entry
C. Tresp, A. Becks, R. Klinkenberg, and J. Hiltner.
Knowledge Representation in a World with Vague Concepts.
In Intelligent Systems: A semiotic perspective, Gaithersburg (USA),
September 1996.
Bibtex entry
C. Tresp, M. Jäger, M. Moser, J. Hiltner, and M. Fathi.
A New Method for Image Segmentation Based on Fuzzy Knowledge.
In Int. IEEE Symposia on Intelligence and Systems, Washington (USA),
Oktober 1996.
Bibtex entry
Back to the homepage of the Chair for Automata Theory.
Generated at Mon Apr 30 13:36:07 CEST 2012.