## Fachbereich Informatik

### Refine

#### Year of publication

- 1999 (267) (remove)

#### Document Type

- Preprint (206)
- Article (52)
- Report (5)
- Master's Thesis (3)
- Study Thesis (1)

#### Keywords

- Case-Based Reasoning (11)
- AG-RESY (6)
- Fallbasiertes Schliessen (5)
- HANDFLEX (5)
- PARO (5)
- case-based problem solving (5)
- Abstraction (4)
- Fallbasiertes Schließen (4)
- Knowledge Acquisition (4)
- resolution (4)

A fundamental variance reduction technique for Monte Carlo integration in the framework of integro-approximation problems is
presented. Using the method of dependent tests a successive hierarchical function approximation algorithm is developed, which
captures discontinuities and exploits smoothness in the target function. The general mathematical scheme and its highly efficient
implementation are illustrated for image generation by ray tracing,
yielding new and much faster image synthesis algorithms.

We study the global solution of Fredholm integral equations of the second kind by the help of Monte Carlo methods. Global solution means that we seek to approximate the full solution function. This is opposed to the usual applications of Monte Carlo, were one only wants to approximate a functional of the solution. In recent years several researchers developed Monte Carlo methods also for the global problem. In this paper we present a new Monte Carlo algorithm for the global solution of integral equations. We use multiwavelet expansions to approximate the solution. We study the behaviour of variance on increasing levels, and based on this, develop a new variance reduction technique. For classes of smooth kernels and right hand sides we determine the convergence rate of this algorithm and show that it is higher
than those of previously developed algorithms for the global problem. Moreover, an information-based complexity analysis shows that our algorithm is optimal among all stochastic algorithms of the same computational
cost and that no deterministic algorithm of the same cost can reach its convergence rate.

Approximation properties of the underlying estimator are used to improve the efficiency of the method of dependent tests. A multilevel approximation procedure is developed such that in each level the number of samples is balanced with the level-dependent variance, resulting in a considerable reduction of the overall computational cost. The new technique is applied to the Monte Carlo estimation of integrals depending on a parameter.

Im Bereich des Software Engineering werden komplexe Software-Entwicklungsprojekte betrachtet. Im Rahmen dieser Projekte werden große Mengen von Informationen bearbeitet. Diese Informationen werden in Software-Artefakten (z.B. in Projektplänen oder Entwicklungsdokumenten, wie Anforderungsbeschreibungen)
festgehalten. Die Artefakte werden während der Entwicklung und der Wartung eines Softwaresystems häufig geändert. Änderungen einer Information in einem Artefakt haben häufig Änderungen
im selben und in anderen Artefakten zur Folge, da Beziehungen innerhalb und zwischen den in den Artefakten festgehaltenen Informationen bestehen. Die Beziehungen liegen meist nicht explizit vor, so daß die Konsequenzen einer Änderung schwer zu überblicken sind. In dieser Arbeit wurde ein Verfolgbarkeitsansatz ausgewählt, der den Benutzer bei der Durchführung von Änderungen an Artefakten unterstützt. Unterstützung bedeutet hierbei, daß der Aufwand zur Durchführung einer Änderung reduziert wird und weniger Fehler bei der Durchführung gemacht werden.
In der Arbeit wurden Anforderungen an einen auszuwählenden Verfolgbarkeitsansatz gestellt. Eine Anforderung war, daß er auf verschiedene Bereiche des Software Engineering, wie z.B. Systementwurf oder Meßplanung, mit jeweils sehr unterschiedlichen Artefakten, anwendbar sein sollte. Die durchgeführte
Literaturrecherche und die anschließende Bewertung anhand der gestellten Anforderungen ergaben, daß das Prinzip der Metamodellierung in Verbindung mit Wissensbankverwaltungssystemen ein geeigneter Verfolgbarkeitsansatz ist. Eine Evaluation, die sich auf Fallstudien aus den Bereichen
"Objektorientierter Entwurf mit UML" und "Meßplanung mit GQM" bezog, ergab, daß das Wissensbankverwaltungssystem
ConceptBase, das auf der Wissensrepräsentationssprache 0-Telos basiert, ein geeignetes Werkzeug zur Unterstützung des Verfolgbarkeitsansatzes ist.

Versions- und Konfigurationsmanagement sind zentrale Instrumente zur intellektuellen Beherrschung komplexer Softwareentwicklungen. In stark wiederverwendungsorientierten Softwareentwicklungsansätzen -wie vom SFB bereitgestellt- muß der Begriff der Konfiguration von traditionell produktorientierten Artefakten auf Prozesse und sonstige Entwicklungserfahrungen erweitert werden. In dieser Veröffentlichung wird ein derartig erweitertes Konfigurationsmodell vorgestellt. Darüberhinau wird eine Ergänzung traditioneller Projektplanungsinformationen diskutiert, die die Ableitung maßgeschneiderter Versions- und Konfigurationsmanagementmechanismen vor Projektbeginn ermöglichen.

The development of complex software systems is driven by many diverse and sometimes contradictory requirements such as correctness and maintainability of resulting products, development costs, and time-to-market. To alleviate these difficulties, we propose a development method for distributed systems that integrates different basic approaches. First, it combines the use of the formal description technique SDL with software reuse concepts. This results in the definition of a use-case driven, incremental development method with SDL-patterns as the main reusable artifacts. Experience with this approach has shown that there are several other factors of influence, such as the quality of reuse artifacts or the experience of the development team. Therefore, we further combined our SDL-pattern approach with an improvement methodology known from the area of experimental software engineering. In order to demonstrate the validity of this integrating approach, we sketch some representative outcomings of a case study.

Die Entwicklung des Zusammenlebens der Menschen geht immer mehr den Weg zur Informations- und Mediengesellschaft. Nicht zuletzt aufgrund der weltweiten Vernetzung ist es uns in minutenschnelle möglich, fast alle erdenklichen Informationen zu Hause auf den Bildschirm geliefert zu bekommen. Es findet sich so jeder zwar in einer gewissen schützenden Anonymität, aber dennoch einer genauso gewollten, wie erschreckenden Transparenz wieder. Jeder klassifiziert in gewisser Weise Informationen, die er preisgibt etwa in öffentliche, persönliche und vertrauliche Nachrichten. Gerade hier müssen Techniken und Methoden bereitstehen, um in dieser anonymen Transparenz Informationen, die nur für spezielle Empfänger gedacht sind vor unbefugtem Zugriff zu schützen und nur denjenigen zugänglich zu machen, die dazu berechtigt sind. Diesen Wunsch hat nicht nur allgemein die Gesellschaft, sondern im speziellen wird die Entwicklung auf diesem Gebiet gerade von staatlichen und militärischen Einrichtungen gefordert und gefördert. So sind häufig eingesetzte Werkzeuge die Methoden der Kryptologie, aber solange es geheime Nachrichten gibt, wird es Angreifer geben, die versuchen, sich unberechtigten Zugang zu diesen Informationen zu verschaffen. Da die ständig wachsende Leistung von EDV-Anlagen das "Knacken" von Verschlüsselungsmethoden begünstigt, muß zu immer sichereren Chiffrierverfahren übergegangen werden. Dieser Umstand macht das Thema Kryptologie für den Moment hochaktuell und auf lange Sicht zu einem zeitlosen Forschungsgebiet der Mathematik und Informatik.

Using an experience factory is one possible concept for supporting and improving reuse in software development. (i.e., reuse of products, processes, quality models, ...). In the context of the Sonderforschungsbereich 501: "Development of Large Systems with Generic methods" (SFB501), the Software Engineering Laboratory (SE Lab) runs such an experience factory as part of the infrastructure services it offers. The SE Lab also provides several tools to support the planning, developing, measuring, and analyzing activities of software development processes. Among these tools, the SE Lab runs and maintains an experience base, the SFB-EB. When an experience factory is utilized, support for experience base maintenance is an important issue. Furthermore, it might be interesting to evaluate experience base usage with regard to the number of accesses to certain experience elements stored in the database. The same holds for the usage of the tools provided by the SE LAB. This report presents a set of supporting tools that were designed to aid in these tasks. These supporting tools check the experience base's consistency and gather information on the usage of SFB-EB and the tools installed in the SE Lab. The results are processed periodically and displayed as HTML result reports (consistency checking) or bar charts (usage profiles).

Manipulating deformable linear objects - Vision-based recognition of contact state transitions -
(1999)

A new and systematic approach to machine vision-based robot manipulation of deformable (non-rigid) linear objects is introduced. This approach reduces the computational needs by using a simple state-oriented model of the objects. These states describe the relation of the object with respect to an obstacle and are derived from the object image and its features. Therefore, the object is segmented from a standard video frame using a fast segmentation algorithm. Several object features are presented which allow the state recognition of the object while being manipulated by the robot.

Comprehensive reuse and systematic evolution of reuse artifacts as proposed by the Quality Improvement Paradigm (QIP) do not only require tool support for mere storage and retrieval. Rather, an integrated management of (potentially reusable) experience data as well as project-related data is needed. This paper presents an approach exploiting object-relational database technology to implement the QIP-driven reuse repository of the SFB 501. Requirements, concepts, and implementational aspects are discussed and illustrated through a running example, namely the reuse and continuous improvement of SDL patterns for developing distributed systems. Based on this discussion, we argue that object-relational database management systems (ORDBMS) are best suited to implement such a comprehensive reuse repository. It is demonstrated how this technology can be used to support all phases of a reuse process and the accompanying improvement cycle. Although the discussions of this paper are strongly related to the requirements of the SFB 501 experience base, the basic realization concepts, and, thereby, the applicability of ORDBMS, can easily be extended to similar applications, i. e., reuse repositories in general.

The paper shows that characterizing the causal relationship between significant events is an important but non-trivial aspect for understanding the behavior of distributed programs. An introduction to the notion of causality and its relation to logical time is given; some fundamental results concerning the characterization of causality are pre- sented. Recent work on the detection of causal relationships in distributed computations is surveyed. The relative merits and limitations of the different approaches are discussed, and their general feasibility is analyzed.

The task of handling non-rigid one-dimensional objects by a robot manipulation system is investigated. To distinguish between different non-rigid object behaviors, five classes of deformable objects from a robotic point of view are proposed. Additionally, an enumeration of all possible contact states of one-dimensional objects with polyhedral obstacles is provided. Finally, the qualitative motion behavior of linear objects is analyzed for stable point contacts. Experiments with different materials validate the analytical results.

We present an approach to learning cooperative behavior of agents. Our ap-proach is based on classifying situations with the help of the nearest-neighborrule. In this context, learning amounts to evolving a set of good prototypical sit-uations. With each prototypical situation an action is associated that should beexecuted in that situation. A set of prototypical situation/action pairs togetherwith the nearest-neighbor rule represent the behavior of an agent.We demonstrate the utility of our approach in the light of variants of thewell-known pursuit game. To this end, we present a classification of variantsof the pursuit game, and we report on the results of our approach obtained forvariants regarding several aspects of the classification. A first implementationof our approach that utilizes a genetic algorithm to conduct the search for a setof suitable prototypical situation/action pairs was able to handle many differentvariants.

The common wisdom that goal orderings can be used to improve planning performance is nearly as old as planning itself. During the last decades of research several approaches emerged that computed goal orderings for different planning paradigms, mostly in the area of state-space planning. For partial-order, plan-space planners goal orderings have not been investigated in much detail. Mechanisms developed for statespace planning are not directly applicable because partial-order planners do not have a current (world) state. Further, it is not completely clear how plan-space planners should make use of goal orderings. This paper describes an approach to extract goal orderings to be used by the plan-space planner CAPlan. The extraction of goal orderings is based on the analysis of an extended version of operator graphs which previously have been found useful for the analysis of interactions and recursion of plan-space planners.

Im Rahmen des Sonderforschungsbereichs SFB314, Projekt X9 "Lernen und Analogie in technischen Expertensystemen", wurde die Verwendbarkeit von Techniken des fallbasierten Schliessens in wissens- basierten Systemen untersucht. Als prototypische Anwendungsdomäne wurde die Arbeitsplanerstellung rotationssymmetrischer Werkstücke gewählt. Im vorliegenden Beitrag wird ein Modell der Arbeits- planerstellung unter Berücksichtigung der verschiedenen, bisher als unabhängig behandelten Planungsmethoden beschrieben. Auf der Basis einer modelbasierte Wissensakquistion aus in Unternehmen verfügbaren Arbeitsplänen wird ein Ausschnitt der Arbeitsplanerstellung, die Aufspannplanung, detailliert. Die Anwendbarkeit wurde durch eine prototypische Realisierung nachgewiesen.

Freivalds, Karpinski and Smith [8] explored a special type of learning in the limit: identification of an unknown concept (function) by eliminating (erasing) all but one possible hypothesis (this type of learning is called co-learning). The motivation behind learning by erasing lies in the process of human and automated computer learning: often we can discard incorrect solutions much easier than to come up with the correct one. In Gödel numberings any learnable family can be learned by an erasing strategy. In this paper we concentrate on co-learning minimal programs. We show that co-learning of minimal programs, as originally defined is significantly weaker than learning minimal programs in Gödel numberings. In order to enhance the learning power

We present an approach to automating the selection of search-guiding heuris-tics that control the search conducted by a problem solver. The approach centerson representing problems with feature vectors that are vectors of numerical val-ues. Thus, similarity between problems can be determined by using a distancemeasure on feature vectors. Given a database of problems, each problem beingassociated with the heuristic that was used to solve it, heuristics to be employedto solve a novel problem are suggested in correspondence with the similaritybetween the novel problem and problems of the database.Our approach is strongly connected with instance-based learning and nearest-neighbor classification and therefore possesses incremental learning capabilities.In experimental studies it has proven to be a viable tool for achieving the finaland crucial missing piece of automation of problem solving - namely selecting anappropriate search-guiding heuristic - in a flexible way.This work was supported by the Deutsche Forschungsgemeinschaft (DFG).

This report presents the properties of a specification of the domain of process planning for rotary symmetrical workpieces. The specification results from a model for problem solving in this domain that involves different reasoners, one of which is an AI planner that achieves goals corresponding to machining workpieces by considering certain operational restrictions of the domain. When planning with SNLP (McAllester and Rosenblitt, 1991), we will show that the resulting plans have the property of minimizing the use of certain key operations. Further, we will show that, for elastic protected plans (Kambhampati et al., 1996) such as the ones produced by SNLP, the goals corresponding to machining parts of a workpiece are OE-constrained trivial serializable, a special form of trivial serializability (Barrett and Weld, 1994). However, we will show that planning with SNLP in this domain can be very difficult: elastic protected plans for machining parts of a workpiece are nonmergeable. Finally, we will show that, for sufix, prefix or sufix and prefix plans such as the ones produced by state-space planners, it is not possible to have both properties, being OEconstrained trivial serializable and minimizing the use of the key operations, at the same time.

In nebenläufigen Systemen erleichtert das Konzept der Atomarität vonOperationen, konkurrierende Zugriffe in größere, leichter beherrschbareAbschnitte zu unterteilen. Wenn wir aber Spezifikationen in der forma-len Beschreibungstechnik Estelle betrachten, erweist es sich, daß es un-ter bestimmten Umständen schwierig ist, die Atomarität der sogenanntenTransitionen bei Implementationen exakt einzuhalten, obwohl diese Ato-marität eine konzeptuelle Grundlage der Semantik von Estelle ist. Es wirdaufgezeigt, wie trotzdem sowohl korrekte als auch effiziente nebenläufigeImplementationen erreicht werden können. Schließlich wird darauf hinge-wiesen, daß die das Problem auslösenden Aktionen oft vom Spezifiziererleicht von vorneherein vermieden werden können; und dies gilt auch überden Kontext von Estelle hinaus.

Top-down and bottom-up theorem proving approaches have each specific ad-vantages and disadvantages. Bottom-up provers profit from strong redundancycontrol and suffer from the lack of goal-orientation, whereas top-down provers aregoal-oriented but have weak calculi when their proof lengths are considered. Inorder to integrate both approaches our method is to achieve cooperation betweena top-down and a bottom-up prover: The top-down prover generates subgoalclauses, then they are processed by a bottom-up prover. We discuss theoreticaspects of this methodology and we introduce techniques for a relevancy-basedfiltering of generated subgoal clauses. Experiments with a model eliminationand a superposition-based prover reveal the high potential of our cooperation approach.The author was supported by the Deutsche Forschungsgemeinschaft (DFG).

We examine an approach for demand-driven cooperative theorem proving.We briefly point out the problems arising from the use of common success-driven cooperation methods, and we propose the application of our approachof requirement-based cooperative theorem proving. This approach allows for abetter orientation on current needs of provers in comparison with conventional co-operation concepts. We introduce an abstract framework for requirement-basedcooperation and describe two instantiations of it: Requirement-based exchangeof facts and sub-problem division and transfer via requests. Finally, we reporton experimental studies conducted in the areas superposition and unfailing com-pletion.The author was supported by the Deutsche Forschungsgemeinschaft (DFG).

HOT is an automated higher-order theorem prover based on HTE, an extensional higher-order tableaux calculus (Kohlhase 95). The first part of the paper introduces a variant of the calculus which closely corresponds to the proof procedure implemented in HOT. The second part discusses HOT's design that can be characterized as a concurrent Blackboard architecture. We show the usefulness of the implementation by including benchmark results for over one hundred solved problems from logic and set theory.

Orderings on polynomial interpretations of operators represent a powerful technique for proving thetermination of rewriting systems. One of the main problems of polynomial orderings concerns thechoice of the right interpretation for a given rewriting system. It is very difficult to develop techniquesfor solving this problem. Here, we present three new heuristic approaches: (i) guidelines for dealingwith special classes of rewriting systems, (ii) an algorithm for choosing appropriate special polynomialsas well as (iii) an extension of the original polynomial ordering which supports the generation ofsuitable interpretations. All these heuristics will be applied to examples in order to illustrate theirpractical relevance.

A large set of criteria to evaluate formal methods for reactive systems is presented. To make this set more comprehensible, it is structured according to a Concept-Model of formal methods. It is made clear that it is necessary to make the catalogue more specific before applying it. Some of the steps needed to do so are explained. As an example the catalogue is applied within the context of the application domain building automation systems to three different formal methods: SDL, statecharts, and a temporallogic.

Im Bereich der Expertensysteme ist das Problemlösen auf der Basis von bekannten Fallbeispielen ein derzeit sehr aktuelles Thema. Auch für Diagnoseaufgaben gewinnt der fallbasierte Ansatz immer mehr an Bedeutung. In diesem Papier soll der im Rahmen des Moltke -Projektes1 an der Universität Kaiserslautern entwickelte fallbasierte Problemlöser Patdex/22 vorgestellt werden. Ein erster Prototyp, Patdex/1, wurde bereits 1988 entwickelt.

We present a mathematical knowledge base containing the factual know-ledge of the first of three parts of a textbook on semi-groups and automata,namely "P. Deussen: Halbgruppen und Automaten". Like almost all math-ematical textbooks this textbook is not self-contained, but there are somealgebraic and set-theoretical concepts not being explained. These concepts areadded to the knowledge base. Furthermore there is knowledge about the nat-ural numbers, which is formalized following the first paragraph of "E. Landau:Grundlagen der Analysis".The data base is written in a sorted higher-order logic, a variant of POST ,the working language of the proof development environment OmegaGamma mkrp. We dis-tinguish three different types of knowledge: axioms, definitions, and theorems.Up to now, there are only 2 axioms (natural numbers and cardinality), 149definitions (like that for a semi-group), and 165 theorems. The consistency ofsuch knowledge bases cannot be proved in general, but inconsistencies may beimported only by the axioms. Definitions and theorems should not lead to anyinconsistency since definitions form conservative extensions and theorems areproved to be consequences.

Das System ART (ASF RRL Translation) stellt im wesentlichen eine Umgebung dar,in welcher die Modularisierbarkeit von Beweisen (Induktionsbeweisen über Gleichungs-spezifikationen) untersucht werden kann. Es wurde die bereits bestehende Spezifikati-onsprache ASF (siehe [BeHeKl89]), in welcher modularisierte Spezifikationen möglichsind, so erweitert, daß zusätzlich auch Beweisaufgaben spezifiziert werden können. Imfolgenden wird diese erweiterte Spezifikationsprache auch ASF genannt. Als Bewei-ser für die Beweisaufgaben einer Spezifikation wurde RRL (siehe [KaZh89]) gewählt.RRL kann sowohl Kommandos aus einem File abarbeiten, wie auch Sitzungsprotokolleanfertigen, mit deren Hilfe sich die Beweisverläufe und Benutzereingaben der entspre-chenden RRL-Sitzung rekonstruieren lassen. In ART kann nun eine ASF-Spezifikation,die Beweisaufgaben umfassen kann, in ein File übersetzt werden, welches von RRLabgearbeitet werden kann. Dies wird im folgenden kurz mit 'Übersetzung von ASF nach RRL' bezeichnet. Bei der Abarbeitung eines solchen Files wird von RRL ein Sit-zungsprotokoll angelegt. ART kann dieses Sitzungsprotokoll dazu heranziehen, neueErgebnisse, wie etwa den erfolgreichen Beweis einer Beweisaufgabe, zu ermitteln, umdiese Ergebnisse der ursprüngliche Spezifikation hinzuzufügen. Dies wird im folgendenkurz mit 'Rückübersetzung von RRL nach ASF' bezeichnet. Im Kern besteht ART alsoaus einer Komponente zur Übersetzung von ASF nach RRL und aus einer Komponentezur Rückübersetzung von RRL nach ASF.

Die systematische Verbesserung von Techniken zur Entwicklung und Betreuung von Software setzt eine explizite Darstellung der in einem Projekt ablaufenden Vorgnge (Prozesse) voraus. Diese Darstellungen (Prozemodelle) werden durch Software- Prozemodellierung gewonnen. Eine Sprache zur Beschreibung solcher Modelle ist MVP-L. Verschiedene Standard-Prozemodelle existieren bereits. Bisher gibt es jedoch kaum dokumentierte Software-Entwicklungsprozesse, die speziell fr die Entwicklung reaktiver Systeme entworfen worden sind, d. h. auf die besonderen Anfordernisse bei der Entwicklung reaktiver Systeme zugeschnitten sind. Auch ist bisher nur wenig Erfahrung dokumentiert, fr welche Art von Projektkontexten diese Prozesse gltig sind. Eine Software- Entwicklungsmethode, die - mit Einschrnkungen - zur Entwicklung reaktiver Systeme geeignet ist, ist SOMT (SDL-oriented Object Modeling Technique). Dieser Bericht beschreibt die erfahrungsbasierte Modellierung der Software-Entwicklungsprozesse von SOMT mit MVP-L. Zunchst werden inhaltliche Grundlagen der Software-Entwicklungsmethode SOMT beschrieben. Insbesondere wird auf die eingesetzten Techniken und deren Kombination eingegangen. Anschlieend werden mgliche Projektkontexte charakterisiert, in denen das SOMT-Modell im Sinne eines Erfahrungselements Gltigkeit hat. Darauf werden der Modellierungsvorgang sowie hierbei gemachte Erfahrungen dokumentiert. Eine vollstndige Darstellung des Modells in grafischer MVP-L-Notation befindet sich im Anhang. Die Darstellung des Modells in textueller Notation kann der SFB-Erfahrungsdatenbank entnommen werden.

In order to improve the quality of software systems and to set up a more effective process for their development, many attempts have been made in the field of software engineering. Reuse of existing knowledge is seen as a promising way to solve the outstanding problems in this field. In previous work we have integrated the design pattern concept with the formal design language SDL, resulting in a certain kind of pattern formalization. For the domain of communication systems we have also developed a pool of SDL patterns with an accompanying process model for pattern application. In this paper we present an extension that combines the SDL pattern approach with the experience base concept. This extension supports a systematic method for empirical evaluation and continuous improvement of the SDL pattern approach. Thereby the experience base serves as a repository necessary for effective reuse of the captured knowledge. A comprehensive usage scenario is described which shows the advantages of the combined approach. To demonstrate its feasibility, first results of a research case study are given.

Ziel dieser Arbeit ist es, eine Methode zur Verfügung zu stellen, mit der ein Simulator für gebäudespezifische Aufgaben modelliert werden kann. Die Modellierung muß dabei so angelegt sein, daß sowohl einfache als auch sehr komplexe Simulatoren für spezielle Gebäude entworfen werden können. Aus dem erstellten Modell ist es anschließend möglich, mit Hilfe von Generatoren automatisch ein Programm zu erzeugen. Dadurch kann ein Entwerfer ohne spezielle Kenntnisse auf dem Gebiet der Simulation einen Gebäude-Simulator entwickeln. Zur Modellierung wurde ein domänenspezifischer Katalog von Entwurfsmustern erstellt. Dabei können die einzelnen Muster direkt zur Modellierung und Codegenerierung eingesetzt werden.

The purpose of this expose is to explain the generic design of a customized communication subsystem. The expose addresses both functional and non-functional aspects. Starting point is a real-time requirement from the application area building automation. We show how this application requirement and some background information about the application area lead to a system architecture, a communication service, a protocol architecture and to the selection, adaptation, and composition of protocol functionalities. The reader will probably be surprised how much effort is necessary in order to implement the innocuous, innocent, inconspicuous looking application requirement. Formal description techniques (FDTs) will be used in all design phases.

Today's communication systems are typically structured into several layers, where each layer realizes a fixed set of protocol functionalities. These functionalities have been carefully chosen such that a wide range of applications can be supported and protocols work in a general environment of networks. However, due to evolving network technologies as well as increased and varying demands of modern applications general-purpose protocol stacks are not always adequate. To improve this situation new flexible communication architectures have been developed which enable the configuration of customized communication subsystems by composing a proper set of reusable building blocks. In particular, several approaches to automatic configuration of communication subsystems have been reported in the literature. This report gives an overview of theses approaches (F-CCS, Da CaPo, x-Kernel, and ADAPTIVE) and, in particular, defines a framework, which identifies common architectural issues and configuration tasks.

A new approach for modelling time that does not rely on the concept of a clock is proposed. In order to establish a notion of time, system behaviour is represented as a joint progression of multiple threads of control, which satisfies a certain set of axioms. We show that the clock-independent time model is related to the well-known concept of a global clock and argue that both approaches establish the same notion of time.

Due to the large variety of modern applications and evolving network technologies, a small number of general-purpose protocol stacks will no longer be sufficient. Rather, customization of communication protocols will play a major role. In this paper, we present an approach that has the potential to substantially reduce the effort for designing customized protocols. Our approach is based on the concept of design patterns, which is well-established in object oriented software development. We specialize this concept to communication protocols, and - in addition - use formal description techniques (FDTs) to specify protocol design patterns as well as rules for their instantiation and composition. The FDTs of our choice are SDL-92 and MSCs, which offer suitable language support. We propose an SDL pattern description template and relate pattern-based configuring of communication protocols to existing SDL methodologies. Particular SDL patterns and the configuring of a customized resource reservation protocol are presented in detail.

A non-trivial real-time requirement obeying a pattern that can be foundin various instantiations in the application domain building automation, and which is therefore called generic, is investigated in detail. Starting point is a description of a real-time problem in natural language augmented by a diagram, in a style often found in requirements documents. Step by step, this description is made more precise and finally transformed into a surprisingly concise formal specification, written in real-time temporal logic with customized operators. Wereason why this formal specification precisely captures the original description- as far as this is feasible due to the lack of precision of natural language.

A Tailored Real Time Temporal Logic for Specifying Requirements of Building Automation Systems
(1999)

A tailored real time temporal logic for specifying requirements of building automation systems is introduced and analyzed. The logic features several new real time operators, which are chosen with regard to the application area. The new operators improve the conciseness and readability of requirements as compared to a general-purpose real time temporal logic. In addition, some of the operators also enhance the expressiveness of the logic. A number of properties of the new operators are presented and proven.

A generic approach to the formal specification of system requirements is presented. It is based on a pool of requirement patterns, which are related to design patterns well-known in object-oriented software development. The application of such patterns enhances the reusability and genericity as well as the intelligibility of the formal requirement specification. The approach is instantiated by a tailored real-time temporal logic and by selecting building automation systems as application domain. With respect to this domain, the pattern discovery and reuse tasks are explained and illustrated, and a set of typical requirement patterns is presented. Finally, the results of a case study where the approach has been applied are summarized.

The background of this paper is the area of case-based reasoning. This is a reasoning technique where one tries to use the solution of some problem which has been solved earlier in order to obta in a solution of a given problem. As example of types of problems where this kind of reasoning occurs very often is the diagnosis of diseases or faults in technical systems. In abstract terms this reduces to a classification task. A difficulty arises when one has not just one solved problem but when there are very many. These are called "cases" and they are stored in the case-base. Then one has to select an appropriate case which means to find one which is "similar" to the actual problem. The notion of similarity has raised much interest in this context. We will first introduce a mathematical framework and define some basic concepts. Then we will study some abstract phenomena in this area and finally present some methods developed and realized in a system at the University of Kaiserslautern.

We present a cooperation concept for automated theorem provers that isbased on a periodical interchange of selected results between several incarnationsof a prover. These incarnations differ from each other in the search heuristic theyemploy for guiding the search of the prover. Depending on the strengths' andweaknesses of these heuristics different knowledge and different communicationstructures are used for selecting the results to interchange.Our concept is easy to implement and can easily be integrated into alreadyexisting theorem provers. Moreover, the resulting cooperation allows the dis-tributed system to find proofs much faster than single heuristics working alone.We substantiate these claims by two case studies: experiments with the DiCoDesystem that is based on the condensed detachment rule and experiments with theSPASS system, a prover for first order logic with equality based on the super-position calculus. Both case studies show the improvements by our cooperationconcept.

This paper presents a new kind of abstraction, which has been developed for the purpose of proofplanning. The basic idea of this paper is to abstract a given theorem and to find an abstractproof of it. Once an abstract proof has been found, this proof has to be refined to a real proofof the original theorem. We present a goal oriented abstraction for the purpose of equality proofplanning, which is parameterized by common parts of the left- and right-hand sides of the givenequality. Therefore, this abstraction technique provides an abstract equality problem which ismore adequate than those generated by the abstractions known so far. The presented abstractionalso supports the heuristic search process based on the difference reduction paradigm. We give aformal definition of the abstract space including the objects and their manipulation. Furthermore,we prove some properties in order to allow an efficient implementation of the presented abstraction.

This report is a first attempt of formalizing the diagonalization proof technique.We give a strategy how to systematically construct diagonalization proofs: (i) findingan indexing relation, (ii) constructing a diagonal element, and (iii) making the implicitcontradiction of the diagonal element explicit. We suggest a declarative representationof the strategy and describe how it can be realized in a proof planning environment.

We examine different possibilities of coupling saturation-based theorem pro-vers by exchanging positive/negative information. We discuss which positive ornegative information is well-suited for cooperative theorem proving and show inan abstract way how this information can be used. Based on this study, we in-troduce a basic model for cooperative theorem proving. We present theoreticalresults regarding the exchange of positive/negative information as well as practi-cal methods and heuristics that allow for a gain of efficiency in comparison withsequential provers. Finally, we report on experimental studies conducted in theareas condensed detachment, unfailing completion, and superposition.The author was supported by the Deutsche Forschungsgemeinschaft (DFG).

Case-based knowledge acquisition, learning and problem solving for diagnostic real world tasks
(1999)

Within this paper we focus on both the solution of real, complex problems using expert system technology and the acquisition of the necessary knowledge from a case-based reasoning point of view. The development of systems which can be applied to real world problems has to meet certain requirements. E.g., all available information sources have to be identified and utilized. Normally, this involves different types of knowledge for which several knowledge representation schemes are needed, because no scheme is equally natural for all sources. Facing empirical knowledge it is important to complement the use of manually compiled, statistic and otherwise induced knowledge by the exploitation of the intuitive understandability of case-based mechanisms. Thus, an integration of case-based and alternative knowledge acquisition and problem solving mechanisms is necessary. For this, the basis is to define the "role" which case-based inference can "play" within a knowledge acquisition workbench. We will discuss a concrete casebased architecture, which has been applied to technical diagnosis problems, and its integration into a knowledge acquisition workbench which includes compiled knowledge and explicit deep models, additionally.

Proof planning is an alternative methodology to classical automated theorem prov-ing based on exhausitve search that was first introduced by Bundy [8]. The goal ofthis paper is to extend the current realm of proof planning to cope with genuinelymathematical problems such as the well-known limit theorems first investigated for au-tomated theorem proving by Bledsoe. The report presents a general methodology andcontains ideas that are new for proof planning and theorem proving, most importantlyideas for search control and for the integration of domain knowledge into a general proofplanning framework. We extend proof planning by employing explicit control-rules andsupermethods. We combine proof planning with constraint solving. Experiments showthe influence of these mechanisms on the performance of a proof planner. For instance,the proofs of LIM+ and LIM* have been automatically proof planned in the extendedproof planner OMEGA.In a general proof planning framework we rationally reconstruct the proofs of limittheorems for real numbers (IR) that were first computed by the special-purpose programreported in [6]. Compared with this program, the rational reconstruction has severaladvantages: It relies on a general-purpose problem solver; it provides high-level, hi-erarchical representations of proofs that can be expanded to checkable ND-proofs; itemploys declarative contol knowledge that is modularly organized.

In this paper we present an extensional higher-order resolution calculus that iscomplete relative to Henkin model semantics. The treatment of the extensionality princi-ples - necessary for the completeness result - by specialized (goal-directed) inference rulesis of practical applicability, as an implentation of the calculus in the Leo-System shows.Furthermore, we prove the long-standing conjecture, that it is sufficient to restrict the orderof primitive substitutions to the order of input formulae.

We present a methodology for coupling several saturation-based theoremprovers (running on different computers). The methodology is well-suited for re-alizing cooperation between different incarnations of one basic prover. Moreover,also different heterogeneous provers - that differ from each other in the calculusand in the heuristic they employ - can be coupled. Cooperation between the dif-ferent provers is achieved by periodically interchanging clauses which are selectedby so-called referees. We present theoretic results regarding the completeness ofthe system of cooperating provers as well as describe concrete heuristics for de-signing referees. Furthermore, we report on two experimental studies performedwith homogeneous and heterogeneous provers in the areas superposition and un-failing completion. The results reveal that the occurring synergetic effects leadto a significant improvement of performance.

Rules are an important knowledge representation formalism in constructive problem solving. On the other hand, object orientation is an essential key technology for maintaining large knowledge bases as well as software applications. Trying to take advantage of the benefits of both paradigms, we integrated Prolog and Smalltalk to build a common base architecture for problem solving. This approach has proven to be useful in the development of two knowledge-based systems for planning and configuration design (CAPlan and Idax). Both applications use Prolog as an efficient computational source for the evaluation of knowledge represented as rules.

Problem specifications for classical planners based on a STRIPS-like representation typically consist of an initial situation and a partially defined goal state. Hierarchical planning approaches, e.g., Hierarchical Task Network (HTN) Planning, have not only richer representations for actions but also for the representation of planning problems. The latter are defined by giving an initial state and an initial task network in which the goals can be ordered with respect to each other. However, studies with a specification of the domain of process planning for the plan-space planner CAPlan (an extension of SNLP) have shown that even without hierarchical domain representation typical properties called goal orderings can be identified in this domain that allow more efficient and correct case retrieval strategies for the case-based planner CAPlan/CbC. Motivated by that, this report describes an extension of the classical problem specifications for plan-space planners like SNLP and descendants. These extended problem specifications allow to define a partial order on the planning goals which can interpreted as an order in which the solution plan should achieve the goals. These goal ordering can theoretically and empirically be shown to improve planning performance not only for case-based but also for generative planning. As a second but different way we show how goal orderings can be used to address the control problem of partial order planners. These improvements can be best understood with a refinement of Barrett's and Weld's extended taxonomy of subgoal collections.

Abstraction is one of the most promising approaches to improve the performance of problem solvers. In several domains abstraction by dropping sentences of a domain description - as used in most hierarchical planners - has proven useful. In this paper we present examples which illustrate significant drawbacks of abstraction by dropping sentences. To overcome these drawbacks, we propose a more general view of abstraction involving the change of representation language. We have developed a new abstraction methodology and a related sound and complete learning algorithm that allows the complete change of representation language of planning cases from concrete to abstract. However, to achieve a powerful change of the representation language, the abstract language itself as well as rules which describe admissible ways of abstracting states must be provided in the domain model. This new abstraction approach is the core of PARIS (Plan Abstraction and Refinement in an Integrated System), a system in which abstract planning cases are automatically learned from given concrete cases. An empirical study in the domain of process planning in mechanical engineering shows significant advantages of the proposed reasoning from abstract cases over classical hierarchical planning.^

We are going to present two methods that allow to exploit previous expe-rience in the area of automated deduction. The first method adapts (learns)the parameters of a heuristic employed for controlling the application of infer-ence rules in order to find a known proof with as little redundant search effortas possible. Adaptation is accomplished by a genetic algorithm. A heuristiclearned that way can then be profitably used to solve similar problems. Thesecond method attempts to re-enact a known proof in a flexible manner in orderto solve an unknown problem whose proof is believed to lie in (close) vicinity.The experimental results obtained with an equational theorem prover show thatthese methods not only allow for impressive speed-ups, but also make it possibleto handle problems that were out of reach before.

This technical report is a compilation of several papers on the task of solving diagnostic problems with the help of topology preserving maps. It first reviews the application of Kohonen's Self- Organizing Feature Map (SOFM) for a technical diagnosis task, namely the fault detection in CNC-Machines with the KoDiag system [RW93], [RW94]. For emergent problems with coding attribute values, we then introduce fuzzy coding, similarity assignment and weight updating schemes for three crucial data types (continuous values, ordered and unordered symbols). These techniques result in a SOFM type network based on user defined local similarities, thus being able to incorporate a priori knowledge about the domain [Rah95].

Real world planning tasks like manufacturing process planning often don't allow to formalize all of the relevant knowledge. Especially, preferences between alternatives are hard to acquire but have high influence on the efficiency of the planning process and the quality of the solution. We describe the essential features of the CAPlan planning architecture that supports cooperative problem solving to narrow the gap caused by absent preference and control knowledge. The architecture combines an SNLP-like base planner with mechanisms for explict representation and maintenance of dependencies between planning decisions. The flexible control interface of CAPlan allows a combination of autonomous and interactive planning in which a user can participate in the problem solving process. Especially, the rejection of arbitrary decisions by a user or dependency-directed backtracking mechanisms are supported by CAPlan.

In this report, we first propose a dichotomy of topology preserving network models based on the degree to which the structure of a network is determined by the given task. We then look closer at one of those groups and investigate the information that is contained in the graph structure of a topology preserving neural network. The task we have in mind is the usage of the network's topology for the retrieval of nearest neighbors of a neuron or a query, as it is of importance, e.g., in medical diagnosis systems. In general considerations, we propose certain properties of the structure and formulate the respective expectable results of network interpretation. From the results we conclude that both topology preservation as well as neuron distribution are highly influential for the network semantics. After a short survey on hierarchical models for data analysis, we propose a new network model that fits both needs. This so called SplitNet model dynamically constructs a hierarchically structured network that provides interpretability by neuron distribution, network topology and hierarchy of the network layers. We present empirical results for this new model and demonstrate its application in the medical domain of nerve lesion diagnosis. Further, we explain a view how the interpretation of the hierarchy in models like SplitNet can be understood in the context of integration of symbolic and connectionist learning.

A straightforward formulation of a mathematical problem is mostly not ad-equate for resolution theorem proving. We present a method to optimize suchformulations by exploiting the variability of first-order logic. The optimizingtransformation is described as logic morphisms, whose operationalizations aretactics. The different behaviour of a resolution theorem prover for the sourceand target formulations is demonstrated by several examples. It is shown howtactical and resolution-style theorem proving can be combined.

Deduktionssysteme
(1999)

Planverfahren
(1999)

We show how to buildup mathematical knowledge bases usingframes. We distinguish three differenttypes of knowledge: axioms, definitions(for introducing concepts like "set" or"group") and theorems (for relating theconcepts). The consistency of such know-ledge bases cannot be proved in gen-eral, but we can restrict the possibilit-ies where inconsistencies may be impor-ted to very few cases, namely to the oc-currence of axioms. Definitions and the-orems should not lead to any inconsisten-cies because definitions form conservativeextensions and theorems are proved to beconsequences.

In most cases higher-order logic is based on the (gamma)-calculus in order to avoid the infinite set of so-called comprehension axioms. However, there is a price to be paid, namelyan undecidable unification algorithm. If we do not use the(gamma) - calculus, but translate higher-order expressions intofirst-order expressions by standard translation techniques, we haveto translate the infinite set of comprehension axioms, too. Ofcourse, in general this is not practicable. Therefore such anapproach requires some restrictions such as the choice of thenecessary axioms by a human user or the restriction to certainproblem classes. This paper will show how the infinite class ofcomprehension axioms can be represented by a finite subclass,so that an automatic translation of finite higher-order prob-lems into finite first-order problems is possible. This trans-lation is sound and complete with respect to a Henkin-stylegeneral model semantics.

Extending existing calculi by sorts is astrong means for improving the deductive power offirst-order theorem provers. Since many mathemat-ical facts can be more easily expressed in higher-orderlogic - aside the greater power of higher-order logicin principle - , it is desirable to transfer the advant-ages of sorts in the first-order case to the higher-ordercase. One possible method for automating higher-order logic is the translation of problem formulationsinto first-order logic and the usage of first-order the-orem provers. For a certain class of problems thismethod can compete with proving theorems directlyin higher-order logic as for instance with the TPStheorem prover of Peter Andrews or with the Nuprlproof development environment of Robert Constable.There are translations from unsorted higher-order lo-gic based on Church's simple theory of types intomany-sorted first-order logic, which are sound andcomplete with respect to a Henkin-style general mod-els semantics. In this paper we extend correspond-ing translations to translations of order-sorted higher-order logic into order-sorted first-order logic, thus weare able to utilize corresponding first-order theoremprover for proving higher-order theorems. We do notuse any (lambda)-expressions, therefore we have to add so-called comprehension axioms, which a priori makethe procedure well-suited only for essentially first-order theorems. However, in practical applicationsof mathematics many theorems are essentially first-order and as it seems to be the case, the comprehen-sion axioms can be mastered too.

In this paper we generalize the notion of method for proofplanning. While we adopt the general structure of methods introducedby Alan Bundy, we make an essential advancement in that we strictlyseparate the declarative knowledge from the procedural knowledge. Thischange of paradigm not only leads to representations easier to under-stand, it also enables modeling the important activity of formulatingmeta-methods, that is, operators that adapt the declarative part of exist-ing methods to suit novel situations. Thus this change of representationleads to a considerably strengthened planning mechanism.After presenting our declarative approach towards methods we describethe basic proof planning process with these. Then we define the notion ofmeta-method, provide an overview of practical examples and illustratehow meta-methods can be integrated into the planning process.

We argue in this paper that sophisticated mi-croplanning techniques are required even formathematical proofs, in contrast to the beliefthat mathematical texts are only schematicand mechanical. We demonstrate why para-phrasing and aggregation significantly en-hance the flexibility and the coherence ofthe text produced. To this end, we adoptedthe Text Structure of Meteer as our basicrepresentation. The type checking mecha-nism of Text Structure allows us to achieveparaphrasing by building comparable combi-nations of linguistic resources. Specified interms of concepts in an uniform ontologicalstructure called the Upper Model, our se-mantic aggregation rules are more compactthan similar rules reported in the literature.

Extending the planADbased paradigm for auto-mated theorem proving, we developed in previ-ous work a declarative approach towards rep-resenting methods in a proof planning frame-work to support their mechanical modification.This paper presents a detailed study of a classof particular methods, embodying variations ofa mathematical technique called diagonaliza-tion. The purpose of this paper is mainly two-fold. First we demonstrate that typical math-ematical methods can be represented in ourframework in a natural way. Second we illus-trate our philosophy of proof planning: besidesplanning with a fixed repertoire of methods,metaADmethods create new methods by modify-ing existing ones. With the help of three differ-ent diagonalization problems we present an ex-ample trace protocol of the evolution of meth-ods: an initial method is extracted from a par-ticular successful proof. This initial method isthen reformulated for the subsequent problems,and more general methods can be obtained byabstracting existing methods. Finally we comeup with a fairly abstract method capable ofdealing with all the three problems, since it cap-tures the very key idea of diagonalization.

Most automated theorem provers suffer from the problem thatthey can produce proofs only in formalisms difficult to understand even forexperienced mathematicians. Effort has been made to reconstruct naturaldeduction (ND) proofs from such machine generated proofs. Although thesingle steps in ND proofs are easy to understand, the entire proof is usuallyat a low level of abstraction, containing too many tedious steps. To obtainproofs similar to those found in mathematical textbooks, we propose a newformalism, called ND style proofs at the assertion level , where derivationsare mostly justified by the application of a definition or a theorem. Aftercharacterizing the structure of compound ND proof segments allowing asser-tion level justification, we show that the same derivations can be achieved bydomain-specific inference rules as well. Furthermore, these rules can be rep-resented compactly in a tree structure. Finally, we describe a system calledPROVERB , which substantially shortens ND proofs by abstracting them tothe assertion level and then transforms them into natural language.

Planning Argumentative Texts
(1999)

This paper presents PROVERB a text planner forargumentative texts. PROVERB's main feature isthat it combines global hierarchical planning and un-planned organization of text with respect to local de-rivation relations in a complementary way. The formersplits the task of presenting a particular proof intosubtasks of presenting subproofs. The latter simulateshow the next intermediate conclusion to be presentedis chosen under the guidance of the local focus.

This paper outlines an implemented system called PROVERB that explains machine -found natural deduction proofs in natural language. Different from earlier works, we pursue a reconstructive approach. Based on the observation that natural deduction proofs are at a too low level of abstraction compared with proofs found in mathematical textbooks, we define first the concept of so-called assertion level inference rules. Derivations justified by these rules can intuitively be understood as the application of a definition or a theorem. Then an algorithm is introduced that abstracts machine-found ND proofs using the assertion level inference rules. Abstracted proofs are then verbalized into natural language by a presentation module. The most significant feature of the presentation module is that it combines standard hierarchical text planning and techniques that locally organize argumentative texts based on the derivation relation under the guidance of a focus mechanism. The behavior of the system is demonstrated with the help of a concrete example throughout the paper.

We describe a technique to make application programs fault tolerant. This techADnique is based on the concept of checkpointing from an active program to one ormore passive backup copies which serve as an abstraction of stable memory. Ifthe primary copy fails, one of the backup copies takes over and resumes processADing service requests. After each failure a new backup copy is created in order torestore the replication degree of the service. All mechanisms necessary to achieveand maintain fault tolerance can be added automatically to the code of a nonADfaulttolerant server, thus making fault tolerance completely transparent for the applicaADtion programmer.

This paper deals with the reference choices involved in thegeneration of argumentative text. A piece of argument-ative text such as the proof of a mathematical theoremconveys a sequence of derivations. For each step of de-rivation, the premises (previously conveyed intermediateresults) and the inference method (such as the applica-tion of a particular theorem or definition) must be madeclear. The appropriateness of these references cruciallyaffects the quality of the text produced.Although not restricted to nominal phrases, our refer-ence decisions are similar to those concerning nominalsubsequent referring expressions: they depend on theavailability of the object referred to within a context andare sensitive to its attentional hierarchy . In this paper,we show how the current context can be appropriatelysegmented into an attentional hierarchy by viewing textgeneration as a combination of planned and unplannedbehavior, and how the discourse theory of Reichmann canbe adapted to handle our special reference problem.

Most automated theorem provers suffer from the problemthat the resulting proofs are difficult to understand even for experiencedmathematicians. An effective communication between the system andits users, however, is crucial for many applications, such as in a mathematical assistant system. Therefore, efforts have been made to transformmachine generated proofs (e.g. resolution proofs) into natural deduction(ND) proofs. The state-of-the-art procedure of proof transformation fol-lows basically its completeness proof: the premises and the conclusionare decomposed into unit literals, then the theorem is derived by mul-tiple levels of proofs by contradiction. Indeterminism is introduced byheuristics that aim at the production of more elegant results. This inde-terministic character entails not only a complex search, but also leads tounpredictable results.In this paper we first study resolution proofs in terms of meaningful op-erations employed by human mathematicians, and thereby establish acorrespondence between resolution proofs and ND proofs at a more ab-stract level. Concretely, we show that if its unit initial clauses are CNFsof literal premises of a problem, a unit resolution corresponds directly toa well-structured ND proof segment that mathematicians intuitively un-derstand as the application of a definition or a theorem. The consequenceis twofold: First it enhances our intuitive understanding of resolutionproofs in terms of the vocabulary with which mathematicians talk aboutproofs. Second, the transformation process is now largely deterministicand therefore efficient. This determinism also guarantees the quality ofresulting proofs.

Even though it is not very often admitted, partial functionsdo play a significant role in many practical applications of deduction sys-tems. Kleene has already given a semantic account of partial functionsusing a three-valued logic decades ago, but there has not been a satisfact-ory mechanization. Recent years have seen a thorough investigation ofthe framework of many-valued truth-functional logics. However, strongKleene logic, where quantification is restricted and therefore not truth-functional, does not fit the framework directly. We solve this problemby applying recent methods from sorted logics. This paper presents atableau calculus that combines the proper treatment of partial functionswith the efficiency of sorted calculi.

The semantics of everyday language and the semanticsof its naive translation into classical first-order language consider-ably differ. An important discrepancy that is addressed in this paperis about the implicit assumption what exists. For instance, in thecase of universal quantification natural language uses restrictions andpresupposes that these restrictions are non-empty, while in classi-cal logic it is only assumed that the whole universe is non-empty.On the other hand, all constants mentioned in classical logic arepresupposed to exist, while it makes no problems to speak about hy-pothetical objects in everyday language. These problems have beendiscussed in philosophical logic and some adequate many-valuedlogics were developed to model these phenomena much better thanclassical first-order logic can do. An adequate calculus, however, hasnot yet been given. Recent years have seen a thorough investigationof the framework of many-valued truth-functional logics. UnfortuADnately, restricted quantifications are not truth-functional, hence theydo not fit the framework directly. We solve this problem by applyingrecent methods from sorted logics.

Even though it is not very often admitted, partial functionsdo play a significant role in many practical applications of deduction sys-tems. Kleene has already given a semantic account of partial functionsusing a three-valued logic decades ago. This approach allows rejectingcertain unwanted formulae as faulty, which the simpler two-valued onesaccept. We have developed resolution and tableau calculi for automatedtheorem proving that take the restrictions of the three-valued logic intoaccount, which however have the severe drawback that existing theo-rem provers cannot directly be adapted to the technique. Even recentlyimplemented calculi for many-valued logics are not well-suited, since inthose the quantification does not exclude the undefined element. In thiswork we show, that it is possible to enhance a two-valued theorem proverby a simple strategy so that it can be used to generate proofs for the the-orems of the three-valued setting. By this we are able to use an existingtheorem prover for a large fragment of the language.

Typical instances, that is, instances that are representative for a particular situ-ation or concept, play an important role in human knowledge representationand reasoning, in particular in analogical reasoning. This wellADknown obser-vation has been a motivation for investigations in cognitive psychology whichprovide a basis for our characterization of typical instances within conceptstructures and for a new inference rule for justified analogical reasoning withtypical instances. In a nutshell this paper suggests to augment the proposi-tional knowledge representation system by a non-propositional part consistingof concept structures which may have directly represented instances as ele-ments. The traditional reasoning system is extended by a rule for justifiedanalogical inference with typical instances using information extracted fromboth knowledge representation subsystems.

This paper addresses two modi of analogical reasoning. Thefirst modus is based on the explicit representation of the justificationfor the analogical inference. The second modus is based on the repre-sentation of typical instances by concept structures. The two kinds ofanalogical inferences rely on different forms of relevance knowledge thatcause non-monotonicity. While the uncertainty and non-monotonicity ofanalogical inferences is not questioned, a semantic characterization ofanalogical reasoning has not been given yet. We introduce a minimalmodel semantics for analogical inference with typical instances.

Dynamic Lambda Calculus
(1999)

The goal of this paper is to lay a logical foundation for discourse theories by providing analgebraic foundation of compositional formalisms for discourse semantics as an analogon tothe simply typed (lambda)-calculus. Just as that can be specialized to type theory by simply providinga special type for truth values and postulating the quantifiers and connectives as constantswith fixed semantics, the proposed dynamic (lambda)-calculus DLC can be specialized to (lambda)-DRT byessentially the same measures, yielding a much more principled and modular treatment of(lambda)-DRT than before; DLC is also expected to eventually provide a conceptually simple basisfor studying higher-order unification for compositional discourse theories.Over the past few years, there have been a series of attempts [Zee89, GS90, EK95, Mus96,KKP96, Kus96] to combine the Montagovian type theoretic framework [Mon74] with dynamicapproaches, such as DRT [Kam81]. The motivation for these developments is to obtain a generallogical framework for discourse semantics that combines compositionality and dynamic binding.Let us look at an example of compositional semantics construction in (lambda)-DRT which is one ofthe above formalisms [KKP96, Kus96]. By the use of fi-reduction we arrive at a first-order DRTrepresentation of the sentence A i man sleeps. (i denoting an index for anaphoric binding.)

Higher-Order Tableaux
(1999)

Even though higher-order calculi for automated theorem prov-ing are rather old, tableau calculi have not been investigated yet. Thispaper presents two free variable tableau calculi for higher-order logicthat use higher-order unification as the key inference procedure. Thesecalculi differ in the treatment of the substitutional properties of equival-ences. The first calculus is equivalent in deductive power to the machine-oriented higher-order refutation calculi known from the literature, whereasthe second is complete with respect to Henkin's general models.

Many mathematical proofs are hard to generate forhumans and even harder for automated theoremprovers. Classical techniques of automated theoremproving involve the application of basic rules, of built-in special procedures, or of tactics. Melis (Melis 1993)introduced a new method for analogical reasoning inautomated theorem proving. In this paper we showhow the derivational analogy replay method is relatedand extended to encompass analogy-driven proof planconstruction. The method is evaluated by showing theproof plan generation of the Pumping Lemma for con-text free languages derived by analogy with the proofplan of the Pumping Lemma for regular languages.This is an impressive evaluation test for the analogicalreasoning method applied to automated theorem prov-ing, as the automated proof of this Pumping Lemmais beyond the capabilities of any of the current auto-mated theorem provers.

This paper addresses the decomposition of proofs as a means of constructingmethods in plan-based automated theorem proving. It shows also, howdecomposition can beneficially be applied in theorem proving by analogy.Decomposition is also useful for human-style proof presentation. We proposeseveral decomposition techniques that were found to be useful in automatedtheorem proving and give examples of their application.

This paper analyzes how mathematicians prove the-orems. The analysis is based upon several empiricalsources such as reports of mathematicians and math-ematical proofs by analogy. In order to combine thestrength of traditional automated theorem provers withhuman-like capabilities, the questions arise: Whichproblem solving strategies are appropriate? Which rep-resentations have to be employed? As a result of ouranalysis, the following reasoning strategies are recog-nized: proof planning with partially instantiated meth-ods, structuring of proofs, the transfer of subproofs andof reformulated subproofs. We discuss the represent-ation of a component of these reasoning strategies, aswell as its properties. We find some mechanisms neededfor theorem proving by analogy, that are not providedby previous approaches to analogy. This leads us to acomputational representation of new components andprocedures for automated theorem proving systems.

This paper shows how a new approach to theorem provingby analogy is applicable to real maths problems. This approach worksat the level of proof-plans and employs reformulation that goes beyondsymbol mapping. The Heine-Borel theorem is a widely known result inmathematics. It is usually stated in R 1 and similar versions are also truein R 2 , in topology, and metric spaces. Its analogical transfer was proposedas a challenge example and could not be solved by previous approachesto theorem proving by analogy. We use a proof-plan of the Heine-Boreltheorem in R 1 as a guide in automatically producing a proof-plan of theHeine-Borel theorem in R 2 by analogy-driven proof-plan construction.

This paper addresses a model of analogy-driven theorem proving that is more general and cognitively more adequate than previous approaches. The model works at the level ofproof-plans. More precisely, we consider analogy as a control strategy in proof planning that employs a source proof-plan to guide the construction of a proof-plan for the target problem. Our approach includes a reformulation of the source proof-plan. This is in accordance with the well known fact that constructing ananalogy in maths often amounts to first finding the appropriate representation which brings out the similarity of two problems, i.e., finding the right concepts and the right level of abstraction. Several well known theorems were processed by our analogy-driven proof-plan construction that could not be proven analogically by previous approaches.

We have developed a middleware framework for workgroup environments that can support distributed software development and a variety of other application domains requiring document management and change management for distributed projects. The framework enables hypermedia-based integration of arbitrary legacy and new information resources available via a range of protocols, not necessarily known in advance to us as the general framework developers nor even to the environment instance designers. The repositories in which such information resides may be dispersed across the Internet and/or an organizational intranet. The framework also permits a range of client models for user and tool interaction, and applies an extensible suite of collaboration services, including but not limited to multi-participant workflow and coordination, to their information retrievals and updates. That is, the framework is interposed between clients, services and repositories - thus "middleware". We explain how our framework makes it easy to realize a comprehensive collection of workgroup and workflow features we culled from a requirements survey conducted by NASA.

Independent development of system components may cause integration problems if their interaction is faulty. This problem may be solved by enforcing required component interactions at the system level. We have developed a system that automatically integrates control-oriented components, to make them consistent with aggregate system behavior re- quirements. Ourmethod is based on the automated synchronization method that modifies independently designed compo-nents to make them satisfy a set of user defined receptive safety properties. The automated synchroniza-tion allows us to design the compo nents as independent controllers that satisfy their individual requirements and to compose a correct executable system by combining the components and enforcing their interaction constraints. This approach gives component designers the freedom to design independently, and produce a functional system by combining the components and specifying their interaction requirements.

An agent-based approach to managing distributed, multi-platform software development projects
(1999)

This paper describes work undertaken within the context of the P3 (Project and Process Prompter) Project which aims to develop the Prompter tool, a 'decision-support tool to assist in the planning and managing of a software development project'. Prompter will have the ability to help software project managers to assimilate best practice and 'know how' in the field of software project management and incorporate expert critiquing to assist with solving the complex problems associated with software project management. This paper focuses on Prompters agent- based approach to tackling the problems of distributed, platform independent support.

Tomorrow's ways of doing business are likely to be far more challenging and interesting than today's due to technological advances that allow people to operate or cooperate anytime, anywhere. Today's workers are becoming mobile without the need of a work home base. Organizations are evolving from the hierarchical lines of control and information flow into more dynamic and flexible structures, where "teams" and individuals are the building blocks for forming task forces and work groups to deal with short and long term project tasks, issues and opportunities. Those individuals and teams will collaborate from their mobile desktops, whether at their offices, home or on the road. A revised paradigm for conducting small and large-scale development and integration is emerging, sometimes called the "virtual enterprise", both in the military and industrial environments. This new paradigm supports communication, cooperation and collaboration of geographically dispersed teams. In this paper we discuss experiences with specific technologies that were investigated by TRW's Infrastructure for Collaboration among Distributed Teams (ICaDT) project; an Independent Research and Development (IR&D) effort.

This paper addresses analogy-driven auto-mated theorem proving that employs a sourceproof-plan to guide the search for a proof-planof the target problem. The approach presen-ted uses reformulations that go beyond symbolmappings and that incorporate frequently usedre-representations and abstractions. Severalrealistic math examples were successfully pro-cessed by our analogy-driven proof-plan con-struction. One challenge example, a Heine-Borel theorem, is discussed here. For this ex-ample the reformulaitons are shown step bystep and the modifying actions are demon-strated.

Analogy in CLAM
(1999)

CL A M is a proof planner, developed by the Dream group in Edinburgh,that mainly operates for inductive proofs. This paper addresses the questionhow an analogy model that I developed independently of CL A M can beapplied to CL A M and it presents analogy-driven proof plan construction as acontrol strategy of CL A M . This strategy is realized as a derivational analogythat includes the reformulation of proof plans. The analogical replay checkswhether the reformulated justifications of the source plan methods hold inthe target as a permission to transfer the method to the target plan. SinceCL A M has very efficient heuristic search strategies, the main purpose ofthe analogy is to suggest lemmas, to replay not commonly loaded methods,to suggest induction variables and induction terms, and to override controlrather than to construct a target proof plan that can be built by CL A Mitself more efficiently.