Karl-Hans Bläsius, Hans-Jürgen Bürckert (eds.):

Ellis Horwood Series in Artificial Intelligence, 1989.

**Abstract: **This book is intended to give the reader an easily
understandable yet comprehensive and up-to-date view of deduction systems.
The book is divided in five chapters. The first chapter (written by J.
Siekmann) gives a review of the history of automated deduction and points
out several applications for deduction systems. Chapter 2 (written by N.
Eisinger and H.J. Ohlbach) introduces the foundations of automated deduction
systems. Chapter 3 deals with equality reasoning (with contributions by
K.-H. Bläsius and H.J. Ohlbach, H.-J. Bürckert, N. Eisinger and
A. Nonnengart). The fourth chapter (written by H.-J. Bürckert) presents
some foundations of logic programming and the last chapter (written by
D. Hutter) provides an introduction to automated theorem proving using
complete induction.

Hans-Jürgen Bürckert:

Matching - a special case of unification?

**Abstract: **Unification is the problem to solve equations of first
order terms by finding (all) substitutions into their variables that make
these two terms equal. Matching is the problem to solve equations, where
only one of the terms has to be instantiated by substitutions. Usually
research in unification theory does not take care of the problems arising
with matching, as it is considered as a special form of unification. We
recall the various definitions of matching from the literature and we compare
matching and unification in a more general framework called restricted
unification. We show that matching and unification in collapse free equational
theories behave similar with respect to the existence and the cardinality
of minimal complete sets of solutions. We present some counterexamples
where matching and unification behave differently, especially we give an
equational theory, in which the existence of solutions for unification
problems is decidable, for matching problems, however, this is undecidable.
Matching and restricted unification as defined here are equivalent to extending
the given signature by free constants. Our counterexamples show that unification
may become undecidable, if we add new free constants to the signature.

Hans-Jürgen Bürckert, Alexander Herold, Manfred Schmidt-Schauß:

On equational theories, unification, and (un)decidability.

**Abstract: **We investigate the following classes of equational
theories which are important in unification theory: permutative, finite,
Noetherian, simple, almost collapse free, collapse free, regualr, and $OMEGA$-free
theories. We show some relationships between the particular clases and
their connections to the unification hierarchy. Especially, we study conditions,
under which minimal and complete sets of unifiers always exist.

We have some undecidability results for the membership problem of equational
theories to these classes (the 'class problem'): simplicity, almost collpase
freeness, and $OMEGA$-freeness are undecidable properties. Finiteness is
known to be also undecidable, and the other investigated properties, permutativity,
regularity, and collapse freeness are knwon to be trivially decidable.

We give an equational theory where every single equation has a minimal
set of unifiers, however, for some systems of equations no minimal set
of unifiers exists. This example suggests that the definition of a unification
problem has to be modified and that the definitions of the unification
types have to be adapted accordingly.

Hans-Jürgen Bürckert:

Lecture Notes in Artificial Intelligence LNAI

**Abstract:** Since the very beginning of the field of automated
deduction it has been part of the game to build in theories that allow
for semantic-based treatment of (sub-)formulae. Following this tradition
we propose a (first oder) predicate logic scheme with a very general form
of *restricted quantifiers*. The domain restrictions for the quantifiers
are taken from a set of open formulae over some theory, the restriction
theory. The restrictions act like filters for the values that can be assigned
to the variables bound by such restricted universal or existential quantifiers:
the values have to satisfy the restrictions in some model of the restrcition
theory. Allowing only for universal quantifiers those restrictions can
also be seen as *constraints* for the variables. Thus we get as an
instance *a constrained logic scheme*. We present a constrained resolution
principle, prove is soundnes and completeness, and discuss some applications.Ý

Hans-Jürgen Bürckert, H. Jürgen Müller:

RATMAN: Rational Agent Testbed for Multi Agent Networks.

In: Demazeau, Muller (eds.),

**Abstract:** RATMAN, a workbench for the definition and testing
of rational agents in multi-agent environments is described. The special
feature of RATMAN is the specification of such agents with hierarchical
knowledge bases comprising all knowledge levels from sensoric knowledge
to learning capabilities. In all levels knowledge representation languages
shall be provided, which are based on logic. In addition statistical and
documentational features support testing and reporting.

Karl-Hans Bläsius, Hans-Jürgen Bürckert (Hrsg.):

2. erweiterte Auflage. Oldenbourg, 1992.

**Abstract:** Dieses Buch ist die erweiterte Neu-Auflage der deutschen
Ausgabe von Deduction Systems in Artificial Intelligence.
Die ursprünglichen Kapitel wurden überarbeitet und zwei weitere
Kapitel über Beweissysteme mit Logiken höherer Stufe (von M.
Kohlhase) und über Modal- und Temporal-Logik (von A. Nonnengart und
H.J. Ohlbach) wurden integriert.

Franz Baader, Hans-Jürgen Bürckert, Bernhard Nebel, Werner Nutt, Gert Smolka:

On the expressivity of feature logics with negation, functional uncertainty, and sort equations.

**Abstract:** Feature logics are the logical basis for so-called
unification grammars studied in computational linguistics. We investigate
the expressivity of feature terms with negation and the functional uncertainty
construct needed for the description of long-distance dependencies and
obtain the following results: satisfiability of feature terms is undecidable,
sort equations can be internalized, consistency of sort equations is decidable
if there is at least one atom, and consistency of sort equations is undecidable
if there is no atom.

Wray Buntine, Hans-Jürgen Bürckert:

On solving equations and disequations.

**Abstract:** We consider the problem of solving a system of equations
and disequations, also known as disunification. Solutions to disunification
problems are subsitutions for the variables of the problem that make the
two terms of each equation equal, but leave those of the disequations different.
We investigate this in both algebraic and logical context where equality
is defined by an equational theory and more generally by a definite clause
equality theory E. We show how E-disunification can be reduced to E-unification,
that is, solving equations only, and give a disunification algorithm for
theories given a unification algorithm. We sketch how disunification can
be applied to handle negation in logic programming with equality in a similar
style to Comerauer's logic programming with rational trees.

Hans-Jürgen Bürckert:

A resolution principle for constrained logics.

**Abstract:** We introduce a constrained logic scheme with a resolution
principle for clauses whose variables are constrained by a constraint theory.
Constraints can be seen as quantifier restrictions filtering out the values
that any interpretation of the underlying constraint theory can assign
to the variables of a formula with such restricted quantifiers.

We present a resolution principle, where unification is replaced by
testing constraints for satisfiability over the constrait theory. We show
that constrained resolution is osund and complete in that a set of constrained
clauses is unsatisfiable over a constraint theory iff for each model of
the constraint theory we can deduce a constrained empty clause whose (collected)
constraint is satisfiable in that model. We demonstrate that we cannot
get a better result in general. But we give conditions, under which at
most finitely many constrained empty clauses are needed or even better
just one empty clause as in classical resolution, sorted resolution or
resolution with theory unification.

Hans-Jürgen Bürckert:

Terminologies and Rules.

In: v. Luck, Marburger (eds.):

Lecture Notes in Artificial Intelligence LNAI

**Abstract:** Terminological logics have become a well understood
formal basis for taxonomic knowledge representation, both for the semantics
(classically by Tarski models) and for the inference services (like concept
subsumption, instantiation, classification, and realization) of terminological
systems of the KL-ONE family. It has been demonstrated that terminological
reasoning can be realized by efficient and logically complete algorithms
based on tableaux style calculi.

However, representation of and reasoning with terminological information
supports just a rather static form of knowledge representation. Only a
fixed description of a domain can be represented: There is the schematic
description of concepts in the socalled TBox and the instantiation of concepts
by individuals and objects in the ABox of such systems. Terminological
inferences can retrieve implicit information, but cannot be used for deriving
new data.

In order to overcome this restriction terminological systems often
allow for additional rule based formalisms. Those, however, are missing
a clear declarative semantics. In this paper we will sketch several declarative
forms of rule based extensions of terminological systems that have been
developed recently.

Andrea Gräber, Hans-Jürgen Bürckert, Armin Laux:

Terminological reasoning with knowledge and belief.

In: Laux, Wansing (eds.),

Akademie-Verlag, 1995.

**Abstract:** Terminological knowledge representation languages in
the style of Kl-ONE are used to represent the taxonomic and conceptual
knowledge of a problem domain in structured and well-formed way. However,
representing knowledge of an application domain with such a formalism amounts
to describing the relevant part of the "world" by listing the facts that
hold in this part of the world. Subjective information of agents - which
is essential for the representation of multi-agent environments - can only
be expressed in a very limited way. For the representation of subjective
information, modal logics with possible worlds semantics provides a formally
well-founded and well-investigated basis.

In this article we show how modal logics can be employed to integrate
the epistemic operators *knowledge* and *belief* into terminological
knowledge representation languages. We introduce syntax and semantics of
the extended language, and show that satisfiability of finite sets of formulas
is decidable. In particular, it is taken into consideration that knowledge
and belief of agents may influence each other, and this interaction is
described by means of so-called *interaction axioms*.

Bernhard Nebel, Hans-Jürgen Bürckert:

Reasoning about temporal relations:

A maximal tractable subclass of Allen's interval algebra.

**Abstract:** We introduce a new subclass of Allen's interval algebra
we call "ORD-Horn subclass," which is a strict superset of the "pointisable
subclass." We prove that reasoning in the ORD-Horn subclass is a polynomial-time
problem and show that the path-consistency method is sufficient for deciding
satisfiability. Further, using an extensive machine-generated case analysis,
we show that the ORD-Horn subclass is a maximal tractable subclass of the
full algebra. In fact, it is the unique greatest tractable subclass amongst
the subclasses that contain all basic relations.

Hans-Jürgen Bürckert, Bernhard Hollunder, Armin Laux:

On Skolemization in constrained logics.

**Abstract:** Quantification in first-order logic always involves
all elements of the universe. However, it is often more natural to just
quantify over those elements of the universe which satisfy a certain condition.
Constrained logics therefore provide (domain) restricted quantifiers constraining
sets *X* of variables by open formulae *R* - this generalizes
sorted logics where single variables are constrained by sorts (which can
be considered as representing open formulae with one free variable). A
formula *F* preceeded by such a restricted (universal or existential)
quantifier can be read as "*F*holds for all (or for some) elements
satisfying the constraint *R*". Testing such formulae for satisfiability
by an appropriately extended resolution principle, one needs a extended
Skolemization procedure. Differently as for "classical" Skolemization of
first-order logics or of common sorted logics quantification over empty
domains has to be taken into account. In the first part of this article
we present a procedure that transforms formulae with restricted quantifiers
into clauses with constraints using an extended Skolemization for restricted
existential quantifiers. Constrained clauses can be tested on unsatisfiability
by the known *constrained resolution principle*. In the second part
we genralize the constrained resolution principle in such a way that it
allows for further optimization, and we introduce a combination of unification
and constraint solving that can be employed to instantiate this kind of
optimization. Notice that these results especially apply to order-sorted
logics and order-sorted unification even when *empty* sorts are allowed.

Hans-Jürgen Bürckert, Petra Funk, Gero Vierke:

An Intercompany Dispatch Support System for Intermodal Transport Chains.

Hawaii International Conference on System Sciences HICSS-33, 2000.

**Abstract:** A critical problem in aa intermodal transport chain
is the direct meet at the transhipment nodes. This requires information
technology and modern communication facilities as well as much closer collaboration
between all the concerned transport operators in the chain. The TELETRUCK
system - currently under development at the German Research Center for
Artificial Intelligence (Deutsches Forschungszentrum für Künstliche
Intelligenz DFKI GmbH) - is a dispatch support system that tackles those
problems. Intercompany planning, scheduling, and monitoring of intermodal
transport chains will be supported by our system. It aims at providing
smooth access to railway time tables and rail-based transport services
and - much more important - at allowing for the planning of both, exclusively
road-based and combined journeys and showing their cost-effectiveness,
where- and whenever possible. We will describe our approach - based on
intelligent agent technology - both the current state of implementation
and our goal of the very next future.

Hans-Jürgen Bürckert, Klaus Fischer:

Holonic Transport Scheduling with TELETRUCK.

**Abstract:** TELETRUCK is a multiagent-based dispatch support system
developed in close collaboration with forwarders and transport engineers.
The system supports dispatch officers in route planning, fleet management,
and driver scheduling. TELETRUCK allows for dynamic planning and online
optimization of transport orders based on an integration with modern telecommunication
facilities. The TELETRUCK approach uses *holonic* agents, i.e., agents
composed of subagents that act in a corporated way, in order to achieve
a flexible, structured resource management in the planning process.

A brief overview is given of the current implementation status of the
TELETRUCK application prototype. Communication, coordination, and resource
control distinguishing holonic from common multiagent systems are discussed.
The underlying algorithms and protocols are described. Future extensions
of the approach for intermodal and intercompany transport planning are
discussed aiming at a smooth integration of modern transport and telecommunication
networks.

back to my home page

Hans-Jürgen Bürckert (hjb@dfki.de), 21. September 2000.