KLUEDO RSS FeedKLUEDO Dokumente/documents
https://kluedo.ub.uni-kl.de/index/index/
Sat, 04 Mar 2000 00:00:00 +0200Sat, 04 Mar 2000 00:00:00 +0200Experiments in learning prototypical situations for variants of the pursuit game
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/92
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.Jörg Denzinger; Matthias Fuchspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/92Mon, 03 Apr 2000 00:00:00 +0200Distributing equational theorem proving
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/346
In this paper we show that distributing the theorem proving task to several experts is a promising idea. We describe the team work method which allows the experts to compete for a while and then to cooperate. In the cooperation phase the best results derived in the competition phase are collected and the less important results are forgotten. We describe some useful experts and explain in detail how they work together. We establish fairness criteria and so prove the distributed system to be both, complete and correct. We have implementedour system and show by non-trivial examples that drastical time speed-ups are possible for a cooperating team of experts compared to the time needed by the best expert in the team.Jürgen Avenhaus; Jörg Denzingerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/346Mon, 03 Apr 2000 00:00:00 +0200Goal oriented equational theorem proving using team work
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/362
The team work method is a concept for distributing automated theoremprovers and so to activate several experts to work on a given problem. We haveimplemented this for pure equational logic using the unfailing KnuthADBendixcompletion procedure as basic prover. In this paper we present three classes ofexperts working in a goal oriented fashion. In general, goal oriented experts perADform their job "unfair" and so are often unable to solve a given problem alone.However, as a team member in the team work method they perform highly effiADcient, even in comparison with such respected provers as Otter 3.0 or REVEAL,as we demonstrate by examples, some of which can only be proved using teamwork.The reason for these achievements results from the fact that the team workmethod forces the experts to compete for a while and then to cooperate by exADchanging their best results. This allows one to collect "good" intermediate resultsand to forget "useless" ones. Completion based proof methods are frequently reADgarded to have the disadvantage of being not goal oriented. We believe that ourapproach overcomes this disadvantage to a large extend.Jörg Denzinger; Matthias Fuchspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/362Mon, 03 Apr 2000 00:00:00 +0200Analysis and Representation of Equational Proofs Generated by a Distributed Completion Based Proof System
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/363
Automatic proof systems are becoming more and more powerful.However, the proofs generated by these systems are not met withwide acceptance, because they are presented in a way inappropriatefor human understanding.In this paper we pursue two different, but related, aims. First wedescribe methods to structure and transform equational proofs in away that they conform to human reading conventions. We developalgorithms to impose a hierarchical structure on proof protocols fromcompletion based proof systems and to generate equational chainsfrom them.Our second aim is to demonstrate the difficulties of obtaining suchprotocols from distributed proof systems and to present our solutionto these problems for provers using the TEAMWORK method. Wealso show that proof systems using this method can give considerablehelp in structuring the proof listing in a way analogous to humanbehaviour.In addition to theoretical results we also include descriptions onalgorithms, implementation notes, examples and data on a variety ofexamples.Jörg Denzinger; Stephan Schulzpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/363Mon, 03 Apr 2000 00:00:00 +0200Planning for distributed theorem proving: The team work approach
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/368
This paper presents a new way to use planning in automated theorem provingby means of distribution. To overcome the problem that often subtasks fora proof problem can not be detected a priori (which prevents the use of theknown planning and distribution techniques) we use a team of experts that workindependently with different heuristics on the problem. After a certain amount oftime referees judge their results using the impact of the results on the behaviourof the expert and a supervisor combines the selected results to a new startingpoint.This supervisor also selects the experts that can work on the problem inthe next round. This selection is a reactive planning task. We outline whichinformation the supervisor can use to fulfill this task and how this informationis processed to result in a plan or to revise a plan. We also show that the useof planning for the assignment of experts to the team allows the system to solvemany different examples in an acceptable time with the same start configurationand without any consultation of the user.Plans are always subject to changeShin'a'in proverbJörg Denzinger; Martin Kronenburgpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/368Mon, 03 Apr 2000 00:00:00 +0200Completion and Equational Theorem Proving using Taxonomic Constraints
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/381
We present an approach to prove several theorems in slightly different axiomsystems simultaneously. We represent the different problems as a taxonomy, i.e.a tree in which each node inherits all knowledge of its predecessors, and solve theproblems using inference steps on rules and equations with simple constraints,i.e. words identifying nodes in the taxonomy. We demonstrate that a substantialgain can be achieved by using taxonomic constraints, not only by avoiding therepetition of inference steps in the different problems but also by achieving runtimes that are much shorter than the accumulated run times when proving eachproblem separately.Jörg Denzingerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/381Mon, 03 Apr 2000 00:00:00 +0200High Performance ATP Systems by Combining Several AI Methods
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/395
We present a concept for an automated theorem prover that employs a searchcontrol based on ideas from several areas of artificial intelligence (AI). The combi-nation of case-based reasoning, several similarity concepts, a cooperation conceptof distributed AI and reactive planning enables a system using our concept tolearn form previous successful proof attempts. In a kind of bootstrapping processeasy problems are used to solve more and more complicated ones.We provide case studies from two domains of interest in pure equationaltheorem proving taken from the TPTP library. These case studies show thatan instantiation of our architecture achieves a high grade of automation andoutperforms state-of-the-art conventional theorem provers.Jörg Denzinger; Marc Fuchspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/395Mon, 03 Apr 2000 00:00:00 +0200Cooperation in Theorem Proving by Loosely Coupled Heuristics
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/403
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.Dirk Fuchs; Jörg Denzingerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/403Mon, 03 Apr 2000 00:00:00 +0200Using Teamwork for the Distribution of Approximately Solving the Traveling Salesman Problem with Genetic Algorithms
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/404
We present a distributed system, Dott, for approximately solving the Trav-eling Salesman Problem (TSP) based on the Teamwork method. So-calledexperts and specialists work independently and in parallel for given time pe-riods. For TSP, specialists are tour construction algorithms and experts usemodified genetic algorithms in which after each application of a genetic operatorthe resulting tour is locally optimized before it is added to the population. Aftera given time period the work of each expert and specialist is judged by a referee.A new start population, including selected individuals from each expert and spe-cialist, is generated by the supervisor, based on the judgments of the referees.Our system is able to find better tours than each of the experts or specialistsworking alone. Also results comparable to those of single runs can be found muchfaster by a team.Jörg Denzinger; Stephan Scholzpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/404Mon, 03 Apr 2000 00:00:00 +0200Knowledge-based Cooperation between Theorem Provers by Techs
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/411
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.Dirk Fuchs; Jörg Denzingerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/411Mon, 03 Apr 2000 00:00:00 +0200Informal Proceedings of the Annual Meeting of "GI-Fachgruppe Deduktionssysteme"
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/415
This report contains a collection of abstracts for talks given at the "Deduktionstreffen" held at Kaiserslautern, October 6 to 8, 1993. The topics of the talks range from theoretical aspects of term rewriting systems and higher order resolution to descriptions of practical proof systems in various applications. They are grouped together according the following classification: Distribution and Combination of Theorem Provers, Termination, Completion, Functional Programs, Inductive Theorem Proving, Automatic Theorem Proving, Proof Presentation. The Deduktionstreffen is the annual meeting of the Fachgruppe Deduktionssysteme in the Gesellschaft für Informatik (GI), the German association for computer science.Jürgen Avenhaus; Jörg Denzingerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/415Mon, 03 Apr 2000 00:00:00 +0200Intelligente Suche im Internet mit Lernenden Systemen
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/991
Der Trend zu einer immer stärkeren Kopplung von Systemen bei gleichzeitiger Dezentralisierung durch Vernetzung hat dazu geführt, daß Computernutzern auf Wunsch enorme Datenmengen zur Verfügung stehen, die sich einer sinnvollen Bearbeitung durch den Nutzer allein völlig entziehen. Unterschiedliche Repräsentationsformalismen für Informationen, Mehrdeutigkeiten, Redundanz sowie eingeschränkte Verfügbarkeit sowohl von Informationen als auch von Rechenleistung machen konventionelle Suchverfahren unanwendbar. Stattdessen werden Suchverfahren und Programme benötigt, die sich intelligent an unterschiedliche Formalismen anpassen, ihre Handlungen ständig evaluieren und fähig sind, ihre Benutzer individuell zu unterstützen. Schlagwörter wie Knowbots, Search-Engines oder Data-Miningsind deshalb zur Zeit in aller Munde. Ein umfassendes Buch, das die hinter diesen und ähnlichen Schlagwörtern verborgenen Ideen und Konzepte präsentiert, existiert jedoch zur Zeit noch nicht. Dies war für uns die Motivation, das Thema "Intelligente Suche im Internet mit Lernenden Systemen" in einem Seminar zu behandeln. Wir haben damit ein Forschungsgebiet aufgegriffen, das sowohl für alle am LSA beteiligten Gruppen von Interesse ist, aber darüber hinaus aktuell von vielen Seiten aufmerksam beobachtet wird. Daher haben wir uns entschlossen, die Ausarbeitungen, die im Rahmen dieses Seminars von den TeilmehmerInnen erstellt wurden, durch den vorliegenden Bericht einer breiteren Öffentlichkeit zugänglich zu machen. Ralph Bergmann; Jörg Denzingerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/991Tue, 07 Mar 2000 00:00:00 +0100Learning from Previous Proof Experience: A Survey
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/995
We present an overview of various learning techniques used in automated theorem provers. We characterize the main problems arising in this context and classify the solutions to these problems from published approaches. We analyze the suitability of several combinations of solutions for different approaches to theorem proving and place these combinations in a spectrum ranging from provers using very specialized learning approaches to optimally adapt to a small class of proof problems, to provers that learn more general kinds of knowledge, resulting in systems that are less efficient in special cases but show improved performance for a wide range of problems. Finally, we suggest combinations of solutions for various proof philosophies.Jörg Denzinger; Matthias Fuchs; C. Goller; Stephan Schulzpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/995Tue, 07 Mar 2000 00:00:00 +0100Extending automatic theorem proving by planning
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/343
A general concept for combining planning with automatic theorem provingis introduced. From this a system architecture based on the notion of planningtrees, methods and sensors is developed. It is illustrated by examples taken fromthe domain of sorting algorithms.Inger Sonntag; Jörg Denzingerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/343Wed, 01 Sep 1999 00:00:00 +0200