Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Publications
1995
F. Baader.
Computing a Minimal Representation of the Subsumption Lattice of all
Conjunctions of Concepts Defined in a Terminology.
In Proceedings of the International Symposium on Knowledge Retrieval, Use,
and Storage for Efficiency, KRUSE 95, pages 168–178, Santa Cruz, USA,
1995.
Bibtex entry Paper (PS)
Abstract
For a given TBox of a terminological KR system, the classification algorithm
computes (a representation of) the subsumption hierarchy of all concepts introduced
in the TBox. In general, this hierarchy does not contain sufficient information to
derive all subsumption relationships between conjunctions of these concepts.
We show how a method developed in the area of ``formal concept analysis'' for
computing minimal implication bases can be used to determine a minimal
representation of the subsumption
hierarchy between conjunctions of concepts introduced in a TBox.
To this purpose, the subsumption algorithm must be extended such that it yields
(sufficient information about) a counterexample in cases where there is no
subsumption relationship. For the concept language ALC, this additional
requirement does not change the worst-case complexity of the subsumption algorithm.
One advantage of the extended hierarchy is that it is a lattice, and not
just a partial ordering.
F. Baader, M. Buchheit, M.A Jeusfeld, and W. Nutt.
Reasoning About Structured Objects: Knowledge Representation Meets
Databases.
The Knowledge Engineering Review, 10(1):73–76, 1995.
Bibtex entry
F. Baader and B. Hollunder.
Embedding Defaults into Terminological Representation Systems.
J. Automated Reasoning, 14:149–180, 1995.
Bibtex entry Free reprint
Abstract
We consider the problem of integrating Reiter's default logic into
terminological representation systems. It turns out that such an
integration is less straightforward than we expected, considering
the fact that the terminological language is a decidable sublanguage
of first-order logic. Semantically, one has the unpleasant effect that
the consequences of a terminological default theory may be rather
unintuitive, and may even vary with the syntactic structure of equivalent
concept expressions. This is due to the unsatisfactory treatment of open
defaults via Skolemization in Reiter's semantics.
On the algorithmic side, we show that this treatment may lead to an
undecidable default consequence relation, even though our base language is
decidable, and we have only finitely many (open) defaults.
Because of these problems, we then consider a restricted semantics for
open defaults in our terminological default theories: default rules are only
applied to individuals that are explicitly present in the knowledge base.
In this semantics it is possible to compute all extensions of a finite
terminological default theory, which means that this type of default
reasoning is decidable. We describe an algorithm for computing extensions,
and show how the inference procedures of terminological systems can be modified
to give optimal support to this algorithm.
F. Baader and B. Hollunder.
Priorities on Defaults with Prerequisites, and their Application in
Treating Specificity in Terminological Default Logic.
J. Automated Reasoning, 15:41–68, 1995.
Bibtex entry Free reprint
Abstract
In a recent paper we have proposed terminological default logic as a
formalism which combines both means for structured representation of
classes and objects, and for default inheritance of properties. The
major drawback that terminological default logic inherits from general
default logic is that it does not take precedence of more specific defaults
over more general ones into account. This behaviour has already been
criticized in the general context of default logic, but it is all the more
problematic in the terminological case where the emphasis lies on the
hierarchical organization of concepts.
The present paper addresses the problem of modifying terminological default
logic such that more specific defaults are preferred. We assume that the
specificity ordering is induced by the hierarchical organization of concepts,
which means that default information is not taken into account when computing
priorities. It turns out that the existing approaches for expressing priorities
between defaults do not seem to be appropriate for defaults with prerequisites.
Therefore we shall consider an alternative approach for dealing with prioritization
in the framework of Reiter's default logic. The formalism is presented in the
general setting of default logic where priorities are given by an arbitrary partial
ordering on the defaults. We shall exhibit some interesting properties of the new
formalism, compare it with existing approaches, and describe an algorithm for
computing extensions. In the terminological case, we thus obtain an automated
default reasoning procedure that takes specificity into account.
F. Baader and A. Laux.
Terminological Logics with Modal Operators.
In C. Mellish, editor, Proceedings of the 14th International Joint
Conference on Artificial Intelligence, pages 808–814, Montréal,
Canada, 1995. Morgan Kaufmann.
Bibtex entry Abstract
Abstract
Terminological knowledge representation formalisms can be
used to represent objective, time-independent facts about an
application domain. Notions like belief, intentions, and time which
are essential for the representation of multi-agent environments can
only be expressed in a very limited way. For such notions, modal
logics with possible worlds semantics provides a formally well-founded
and well-investigated basis.
This paper presents a framework for integrating modal operators into
terminological knowledge representation languages. These operators can
be used both inside of concept expressions and in front of
terminological and assertional axioms.
We introduce syntax and semantics of the extended language, and show that
satisfiability of finite sets of formulas is decidable, provided that
all modal operators are interpreted in the basic logic {\sf K}, and that the
increasing domain assumption is used.
F. Baader and H.-J. Ohlbach.
A Multi-Dimensional Terminological Knowledge Representation Language.
J. Applied Non-Classical Logics, 5:153–197, 1995.
Bibtex entry
F. Baader and K.U. Schulz.
Combination of Constraint Solving Techniques: An Algebraic Point of
View.
In Proceedings of the 6th International Conference on Rewriting Techniques
and Applications, volume 914 of Lecture Notes in Artificial
Intelligence, pages 352–366, Kaiserslautern, Germany, 1995. Springer
Verlag.
Bibtex entry Abstract
Abstract
In a previous paper we have introduced a method that allows one to combine decision
procedures for unifiability in disjoint equational theories. Lately, it has
turned out that the prerequisite for this method to apply---namely that
unification with so-called linear constant restrictions is decidable in the
single theories---is equivalent to requiring decidability of the positive fragment
of the first order theory of the equational theories. Thus, the combination
method can also be seen as a tool for combining decision procedures for
positive theories of free algebras defined by equational theories.
The present paper uses this observation as the starting point of a more
abstract, algebraic approach to formulating and solving the combination
problem.
Its contributions are twofold. As a new result, we describe an optimization and an
extension of our combination method to the case of constraint solvers that also
take relational constraints (such as ordering constraints) into account.
The second contribution is a new proof method, which
depends on abstract notions and results from universal algebra,
as opposed to technical manipulations of terms (such as ordered
rewriting, abstraction functions, etc.)
F. Baader and K.U. Schulz.
Combination Techniques and Decision Problems for Disunification.
Theoretical Computer Science B, 142:229–255, 1995.
Bibtex entry Free reprint
Abstract
Previous work on combination techniques considered
the question of how to combine unification algorithms for disjoint
equational theories $E_1,\ldots,E_n$ in order to obtain a
unification algorithm for the union $E_1 \cup \ldots\cup E_n$ of the
theories. Here we want to show that variants of this method may be
used to decide solvability and ground solvability
of disunification problems in $E_1 \cup \ldots\cup E_n$. Our first
result says that solvability of disunification
problems in the free algebra of the combined theory
$E_1 \cup \ldots\cup E_n$ is decidable
if solvability of disunification problems with linear constant restrictions
in the free algebras of the theories $E_i$ ($i = 1,\ldots,n$) is
decidable.
In order to decide ground solvability (i.e., solvability in the initial
algebra) of disunification problems in $E_1 \cup \ldots\cup E_n$
we have to consider a new kind of subproblem for the
particular theories $E_i$, namely solvability (in the free algebra)
of disunification problems with linear constant restriction
under the additional constraint that values of variables are not
$E_i$-equivalent to variables.
The correspondence between ground solvability and this new kind of
solvability holds,
{\em (1)} if one theory $E_i$ is the free theory with at least one
function symbol and one constant, or
{\em (2)} if the initial algebras of all theories $E_i$ are
infinite.
Our results can be used to show that the
existential fragment of the theory of the (ground) term algebra
modulo associativity of a finite number of function symbols is
decidable; the same result follows for function symbols
which are associative and commutative, or associative, commutative and
idempotent.
F. Baader and K.U. Schulz.
On the Combination of Symbolic Constraints, Solution Domains, and
Constraint Solvers.
In Proceedings of the International Conference on Principles and Practice
of Constraint Programming, CP95, volume 976 of Lecture Notes in
Artificial Intelligence, pages 380–397, Cassis, France, 1995. Springer
Verlag.
Bibtex entry Abstract
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. Subsequently, we define so-called {\em simply-combinable structures}
(SC-structures). For SC-structures over disjoint signatures,
a canonical amalgamation construction exists, which for the subclass of
{\em strong} SC-structures yields the free amalgamated product.
The combination technique of \cite{BaaderSchulzCADE,BaaderSchulzRTA95}
can be used to combine constraint solvers for (strong) SC-structures over disjoint
signatures into a solver for their (free) amalgamated product.
In addition to term algebras modulo equational theories, the class of SC-structures
contains many solution structures that have been used 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.
Franz Baader and Can Adam Albayrak.
Termersetzungssysteme, Skript zur Vorlesung, volume 12 of
Aachener Beiträge zur Informatik.
Verlag der Augustinus Buchhandlung, Pontstr. 96, D-52062 Aachen, 1995.
ISBN 3-86073-148-3.
Bibtex entry Abstract
Abstract
Termersetzungssysteme sind ein wichtiges Hilfmittel zur automatisierten
Behandlung von Gleichheitsaxiomen, da sie das Rechnen in gleichungsdefinierten
Algebren ermöglichen. Sie finden deshalb zum Beispiel im Bereich der
Algebraischen Spezifikation, der funktionalen Programmierung und des
automatischen Theorembeweisens Verwendung.
Das Skriptum stellt eine ausführliche Einführung in die im Bereich
Termersetzungssysteme wichtigen Begriffe, Methoden und Resultate dar. Es werden
Eigenschaften abstrakter Redunktionssysteme, Wortersetzungssysteme
(Semi-Thue-Systeme), Grundbegriffe aus der universellen Algebra, Konfluenz und
Terminierung von Termersetzungssystemen, Unifikation,
Knuth-Bendix-Vervollständigung, Vervollständigung ohne Abbruch und Termersetzung
modulo Gleichungstheorien behandelt.
Franz Baader and Hans Jürgen Ohlbach.
A Multi-Dimensional Terminological Knowledge Representation Language.
Technical Report MPI-I-95-2-005, Max-Planck-Institut für Informatik,
Saarbrücken, 1995.
Bibtex entry Paper (PS)
Abstract
An extension of the concept description language ALC used in KL-ONE-like
terminological reasoning is presented. The extension includes multi-modal
operators that can either stand for the usual role quantifications or for
modalities such as belief, time etc. The modal operators can be used at all
levels of the concept terms, and they can be used to modify both
concepts and roles. This is an instance of a new kind of combination of modal
logics where the modal operators of one logic may operate directly on the
operators of the other logic. Different versions of this logic are investigated
and various results about decidability and undecidability are
presented. The main problem, however, decidability of the basic version of the
logic, remains open.
François Bergeron and Ulrike Sattler.
Constructible differentially finite algebraic series in several
variables.
Theoretical Computer Science, 144(1-2):59–66, June 1995.
Bibtex entry Abstract
Abstract
We extend the concept of CDF-series to the context of several variables, and
show that the series solution of first order differential equations y=x(t,y) and
functional equations y=x(t,y), with x CDF in two variables, are CDF-series. We
also give many effective closure properties for CDF-series in several variables.
M. Fathi, C. Tresp, K. Holte, and J. Hiltner.
Development of Objective Functions for Soft Computing in Medical
Applications.
In ACM Computing Week, Nashville (USA), Februar 1995.
Bibtex entry
Ulrike Sattler.
A Concept Language for an engeneering application with part-whole
relations.
In A. Borgida, M. Lenzerini, D. Nardi, and B. Nebel, editors, Proceedings
of the International Workshop on Description Logics, pages 119–123,
Rome, 1995.
Bibtex entry Paper (PS)
Abstract
We investigate how terminological knowledge representation systems can be used
to support modeling in an engeneering application. Because of the high
complexity of the application, support of top--down modeling is a quite
ambitious, but useful task for TKR Systems. An interesting problem to solve in
this context is the handling of composite objects. Therefor, not only different
part-whole relations have to be represented (some of them are transitive) but
also their transitivity-like interaction as well as local properties of these
relations. Hence this application calls for a concept language with powerful
role forming operators.
A concept language P with the expressive power to represent part-whole
relations is defined, but it turns out that satisfiability of concept terms in
P is undecidable. Hence it is necessary to drop some (but not many) of
the demands made for the benefit of decidability. Several ways to handle the
high complexity of inference algorithms of P are discussed.
Back to the homepage of the Chair for Automata Theory.
Generated at Mon Apr 30 13:36:07 CEST 2012.