KLUEDO RSS FeedKLUEDO Dokumente/documents
https://kluedo.ub.uni-kl.de/index/index/
Mon, 03 Apr 2000 00:00:00 +0200Mon, 03 Apr 2000 00:00:00 +0200Cooperation between Top-Down and Bottom-Up Theorem Provers by Subgoal Clause Transfer
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/412
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).Dirk Fuchspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/412Mon, 03 Apr 2000 00:00:00 +0200Requirement-based cooperative theorem proving
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/413
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).Dirk Fuchspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/413Mon, 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 +0200Island Planning and Refinement
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/416
Planning for realistic problems in a static and deterministic environment with complete information faces exponential search spaces and, more often than not, should produce plans comprehensible for the user. This article introduces new planning strategies inspired by proof planning examples in order to tackle the search-space-problem and the structured-plan-problem. Island planning and refinement as well as subproblem refinement are integrated into a general planning framework and some exemplary control knowledge suitable for proof planning is given.Erica Melispreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/416Mon, 03 Apr 2000 00:00:00 +0200Model Existence for Higher Order Logic
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/417
In this paper we provide a semantical meta-theory that will support the development of higher-order calculi for automated theorem proving like the corresponding methodology has in first-order logic. To reach this goal, we establish classes of models that adequately characterize the existing theorem-proving calculi, that is, so that they are sound and complete to these calculi, and a standard methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of machine-oriented calculi.Christoph Benzmüller; Michael Kohlhasepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/417Mon, 03 Apr 2000 00:00:00 +0200HOT: A Concurrent Automated Theorem Prover based on Higher-Order Tableaux
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/418
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.Karsten Konradpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/418Mon, 03 Apr 2000 00:00:00 +0200Termination Proofs of Rewriting Systems
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/419
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.Joachim Steinbachpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/419Mon, 03 Apr 2000 00:00:00 +0200Higher-Order Automated Theorem Proving for Natural Language Semantics
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/420
This paper describes a tableau-based higher-order theorem prover HOT and an application to natural language semantics. In this application, HOT is used to prove equivalences using world knowledge during higher-order unification (HOU). This extended form of HOU is used to compute the licensing conditions for corrections.Michael Kohlhase; Karsten Konradpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/420Mon, 03 Apr 2000 00:00:00 +0200Semantical Investigation of Simultaneous Skolemization for First-Order Sequent Calculus
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/421
Simultaneous quantifier elimination in sequent calculus is an improvement over the well-known skolemization. It allows a lazy handling of instantiations as well as of the order of certain reductions. We prove the soundness of a sequent calculus which incorporates a rule for simultaneous quantifier elimination. The proof is performed by semantical arguments and provides some insights into the dependencies between various formulas in a sequent.Serge Autexier; Heiko Mantelpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/421Mon, 03 Apr 2000 00:00:00 +0200Proof Presentation Based on Proof Plans
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/422
The paper addresses two problems of comprehensible proof presentation, the hierarchically structured presentation at the level of proof methods and different presentation styles of construction proofs. It provides solutions for these problems that can make use of proof plans generated by an automated proof planner.Erica Melispreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/422Mon, 03 Apr 2000 00:00:00 +0200Classification and Learning of Similarity Measures
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/331
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.Michael M. Richterpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/331Mon, 03 Apr 2000 00:00:00 +0200PLATIN A Planning System for Inductive Theorem Proving Implementation and Experiences
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/402
This paper provides a description of PLATIN. With PLATIN we present an imple-mented system for planning inductive theorem proofs in equational theories that arebased on rewrite methods. We provide a survey of the underlying architecture ofPLATIN and then concentrate on details and experiences of the current implementa-tion.Robert Eschbach; Inger Sonntagpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/402Mon, 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 +0200An Abstraction for Proof Planning: The S-Abstraction
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/405
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.Serge Autexierpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/405Mon, 03 Apr 2000 00:00:00 +0200Planning Diagonalization Proofs
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/406
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.Lassaad Cheikhrouhoupreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/406Mon, 03 Apr 2000 00:00:00 +0200Coupling Saturation-Based Provers by Exchanging Positive/Negative Information
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/407
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).Dirk Fuchspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/407Mon, 03 Apr 2000 00:00:00 +0200Case-based knowledge acquisition, learning and problem solving for diagnostic real world tasks
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/408
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.Klaus-Dieter Althoff; Stefan Wesspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/408Mon, 03 Apr 2000 00:00:00 +0200Progress in Proof Planning:Planning Limit Theorems Automatically
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/409
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.Erica Melispreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/409Mon, 03 Apr 2000 00:00:00 +0200Henkin Completeness of Higher-Order Resolution
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/410
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.Christoph Benzmüller; Michael Kohlhasepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/410Mon, 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 +0200Adaptation of Declaratively Represented Methods in Proof Planning
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/382
The reasoning power of human-oriented plan-based reasoning systems is primarilyderived from their domain-specific problem solving knowledge. Such knowledge is, how-ever, intrinsically incomplete. In order to model the human ability of adapting existingmethods to new situations we present in this work a declarative approach for represent-ing methods, which can be adapted by so-called meta-methods. Since apparently thesuccess of this approach relies on the existence of general and strong meta-methods,we describe several meta-methods of general interest in detail by presenting the prob-lem solving process of two familiar classes of mathematical problems. These examplesshould illustrate our philosophy of proof planning as well: besides planning with thecurrent repertoire of methods, the repertoire of methods evolves with experience inthat new ones are created by meta-methods which modify existing ones.Xiaorong Huang; Manfred Kerber; Lassaad Cheikhrouhoupreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/382Mon, 03 Apr 2000 00:00:00 +0200Confluence without Termination via Parallel Critical Pairs
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/383
We present a new criterion for confluence of (possibly) non-terminating left-linear term rewriting systems. The criterion is based on certain strong joinabil-ity properties of parallel critical pairs . We show how this criterion relates toother well-known results, consider some special cases and discuss some possibleextensions.Bernhard Gramlichpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/383Mon, 03 Apr 2000 00:00:00 +0200Theorem Proving in Hierarchical Clausal Specifications
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/384
In this paper we are interested in an algebraic specification language that (1) allowsfor sufficient expessiveness, (2) admits a well-defined semantics, and (3) allows for formalproofs. To that end we study clausal specifications over built-in algebras. To keep thingssimple, we consider built-in algebras only that are given as the initial model of a Hornclause specification. On top of this Horn clause specification new operators are (partially)defined by positive/negative conditional equations. In the first part of the paper wedefine three types of semantics for such a hierarchical specification: model-theoretic,operational, and rewrite-based semantics. We show that all these semantics coincide,provided some restrictions are met. We associate a distinguished algebra A spec to ahierachical specification spec. This algebra is initial in the class of all models of spec.In the second part of the paper we study how to prove a theorem (a clause) valid in thedistinguished algebra A spec . We first present an abstract framework for inductive theoremprovers. Then we instantiate this framework for proving inductive validity. Finally wegive some examples to show how concrete proofs are carried out.This report was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)Jürgen Avenhaus; Klaus Madlenerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/384Mon, 03 Apr 2000 00:00:00 +0200Inductive theorem proving in theories specified by positive/negative-conditional equations
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/385
We present an inference system for clausal theorem proving w.r.t. various kinds of inductivevalidity in theories specified by constructor-based positive/negative-conditional equations. The reductionrelation defined by such equations has to be (ground) confluent, but need not be terminating. Our con-structor-based approach is well-suited for inductive theorem proving in the presence of partially definedfunctions. The proposed inference system provides explicit induction hypotheses and can be instantiatedwith various wellfounded induction orderings. While emphasizing a well structured clear design of theinference system, our fundamental design goal is user-orientation and practical usefulness rather thantheoretical elegance. The resulting inference system is comprehensive and relatively powerful, but requiresa sophisticated concept of proof guidance, which is not treated in this paper.This research was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)Claus-Peter Wirth; Ulrich Kühlerpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/385Mon, 03 Apr 2000 00:00:00 +0200