Selected Publications: Abstracts

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. 

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. 

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. 

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.Ý 

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. 

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. 

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. 

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. 

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. 

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. 

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. 

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. 

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 "Fholds 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. 

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. 

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.