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 +0200Analogical Reasoning with Typical Examples
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/337
Typical examples, that is, examples that are representative for a particular situationor concept, play an important role in human knowledge representation and reasoning.In real life situations more often than not, instead of a lengthy abstract characteriza-tion, a typical example is used to describe the situation. This well-known observationhas been the motivation for various investigations in experimental psychology, whichalso motivate our formal characterization of typical examples, based on a partial orderfor their typicality. Reasoning by typical examples is then developed as a special caseof analogical reasoning using the semantic information contained in the correspondingconcept structures. We derive new inference rules by replacing the explicit informa-tion about connections and similarity, which are normally used to formalize analogicalinference rules, by information about the relationship to typical examples. Using theseinference rules analogical reasoning proceeds by checking a related typical example,this is a form of reasoning based on semantic information from cases.Manfred Kerber; Erica Melis; Jörg Siekmannpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/337Mon, 03 Apr 2000 00:00:00 +0200The Adaption of Proof Methods by Reformulation
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/63
Manfred Kerber; Xiaorong Huang; Lassaad Cheikhrouhouarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/63Mon, 03 Apr 2000 00:00:00 +0200Reuse of Proofs by Meta-Methods
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/250
This paper describes a declarative approach forencoding the plan operators in proof planning,the so-called methods. The notion of methodevolves from the much studied concept of a tac-tic and was first used by A. Bundy. Signific-ant deductive power has been achieved withthe planning approach towards automated de-duction; however, the procedural character ofthe tactic part of methods hinders mechanicalmodification. Although the strength of a proofplanning system largely depends on powerfulgeneral procedures which solve a large class ofproblems, mechanical or even automated modi-fication of methods is necessary, since methodsdesigned for a specific type of problems willnever be general enough. After introducing thegeneral framework, we exemplify the mechan-ical modification of methods via a particularmeta-method which modifies methods by trans-forming connectives to quantifiers.Manfred Kerber; Xiaorong Huangpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/250Mon, 03 Apr 2000 00:00:00 +0200Die Beweisentwicklungsumgebung Omega-MKRK
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/251
Die Beweisentwicklungsumgebung Omega-Mkrp soll Mathematiker bei einer ihrer Haupttätigkeiten, nämlich dem Beweisen mathematischer Theoreme unterstützen. Diese Unterstützung muß so komfortabel sein, daß die Beweise mit vertretbarem Aufwand formal durchgeführt werden können und daß die Korrektheit der so erzeugten Beweise durch das System sichergestellt wird. Ein solches System wird sich nur dann wirklich durchsetzen, wenn die rechnergestützte Suche nach formalen Beweisen weniger aufwendig und leichter ist, als ohne das System. Um dies zu erreichen, ergeben sich verschiedene Anforderungen an eine solche Entwicklungsumgebung, die wir im einzelnen beschreiben. Diese betreffen insbesondere die Ausdruckskraft der verwendeten Objektsprache, die Möglichkeit, abstrakt über Beweispläne zu reden, die am Menschen orientierte Präsentation der gefundenen Beweise, aber auch die effiziente Unterstützung beim Füllen von Beweislücken. Das im folgenden vorgestellte Omega-Mkrp-System ist eine Synthese der Ansätze des vollautomatischen, des interaktiven und des planbasierten Beweisens und versucht erstmalig die Ergebnisse dieser drei Forschungsrichtungen in einem System zu vereinigen. Dieser Artikel soll eine Übersicht über unsere Arbeit an diesem System geben.Manfred Kerber; Xiaorong Huang; Michael Kohlhase; Erica Melis; Dan Nesmith; Jörn Richts; Jörg Siekmannpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/251Mon, 03 Apr 2000 00:00:00 +0200A Test for Evaluating the Practical Usefulness of Deduction Systems
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/252
Manfred Kerber; Xiaorong Huang; Michael Kohlhase; Dan Nesmith; Jörn Richtspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/252Mon, 03 Apr 2000 00:00:00 +0200Guaranteeing Correctness through the Communication of Checkable Proofs(or: Would You Really Trust an Automated Reasoning System?)
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/254
Manfred Kerber; Xiaorong Huang; Michael Kohlhase; Dan Nesmith; Jörn Richtspreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/254Mon, 03 Apr 2000 00:00:00 +0200Mechanising Partiality without Re-Implementation
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/267
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.Manfred Kerber; Michael Kohlhasepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/267Mon, 03 Apr 2000 00:00:00 +0200Two Kinds of Non-Monotonic Analogical Inference ?
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/270
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.Manfred Kerber; Erica Melispreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/270Mon, 03 Apr 2000 00:00:00 +0200Analogical Reasoning with a Hybrid Knowledge Base
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/271
Manfred Kerber; Erica Melis; Jörg Siekmannpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/271Mon, 03 Apr 2000 00:00:00 +0200Beherrschbarkeit von Computersystemen
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/273
Manfred Kerber; Axel Präckleinpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/273Mon, 03 Apr 2000 00:00:00 +0200Planverfahren
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/277
Manfred Kerberpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/277Mon, 03 Apr 2000 00:00:00 +0200On the Representation of Mathematical Concepts and their Translation into First-Order Logic
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/334
To prove difficult theorems in a mathematical field requires substantial know-ledge of that field. In this thesis a frame-based knowledge representation formal-ism including higher-order sorted logic is presented, which supports a conceptualrepresentation and to a large extent guarantees the consistency of the built-upknowledge bases. In order to operationalize this knowledge, for instance, in anautomated theorem proving system, a class of sound morphisms from higher-orderinto first-order logic is given, in addition a sound and complete translation ispresented. The translations are bijective and hence compatible with a later proofpresentation.In order to prove certain theorems the comprehension axioms are necessary,(but difficult to handle in an automated system); such theorems are called trulyhigher-order. Many apparently higher-order theorems (i.e. theorems that arestated in higher-order syntax) however are essentially first-order in the sense thatthey can be proved without the comprehension axioms: for proving these theoremsthe translation technique as presented in this thesis is well-suited.Manfred Kerberpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/334Mon, 03 Apr 2000 00:00:00 +0200Tactics for the Improvement of Problem Formulation in Resolution-Based Theorem Proving
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/335
We transform a user-friendly formulation of aproblem to a machine-friendly one exploiting the variabilityof first-order logic to express facts. The usefulness of tacticsto improve the presentation is shown with several examples.In particular it is shown how tactical and resolution theoremproving can be combined.Manfred Kerber; Axel Präckleinpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/335Mon, 03 Apr 2000 00:00:00 +0200Methods - The Basic Units for Planning and Verifying Proofs
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/338
This paper concerns a knowledge structure called method , within a compu-tational model for human oriented deduction. With human oriented theoremproving cast as an interleaving process of planning and verification, the body ofall methods reflects the reasoning repertoire of a reasoning system. While weadopt the general structure of methods introduced by Alan Bundy, we make anessential advancement in that we strictly separate the declarative knowledgefrom the procedural knowledge. This is achieved by postulating some stand-ard types of knowledge we have identified, such as inference rules, assertions,and proof schemata, together with corresponding knowledge interpreters. Ourapproach in effect changes the way deductive knowledge is encoded: A newcompound declarative knowledge structure, the proof schema, takes the placeof complicated procedures for modeling specific proof strategies. This change ofparadigm not only leads to representations easier to understand, it also enablesus modeling the even more important activity of formulating meta-methods,that is, operators that adapt existing methods to suit novel situations. In thispaper, we first introduce briefly the general framework for describing methods.Then we turn to several types of knowledge with their interpreters. Finally,we briefly illustrate some meta-methods.Xiaorong Huang; Manfred Kerber; Michael Kohlhasepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/338Mon, 03 Apr 2000 00:00:00 +0200OMEGA MKRP - A Proof Development Environment
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/340
This report presents the main ideas underlyingtheOmegaGamma mkrp-system, an environmentfor the development of mathematical proofs. The motivation for the development ofthis system comes from our extensive experience with traditional first-order theoremprovers and aims to overcome some of their shortcomings. After comparing the benefitsand drawbacks of existing systems, we propose a system architecture that combinesthe positive features of different types of theorem-proving systems, most notably theadvantages of human-oriented systems based on methods (our version of tactics) andthe deductive strength of traditional automated theorem provers.In OmegaGamma mkrp a user first states a problem to be solved in a typed and sorted higher-order language (called POST ) and then applies natural deduction inference rules inorder to prove it. He can also insert a mathematical fact from an integrated data-base into the current partial proof, he can apply a domain-specific problem-solvingmethod, or he can call an integrated automated theorem prover to solve a subprob-lem. The user can also pass the control to a planning component that supports andpartially automates his long-range planning of a proof. Toward the important goal ofuser-friendliness, machine-generated proofs are transformed in several steps into muchshorter, better-structured proofs that are finally translated into natural language.This work was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D2, D3)Xiaorong Huang; Manfred Kerber; Michael Kohlhase; Erica Melis; Dan Nesmith; Jörn Richts; Jörg Siekmannpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/340Mon, 03 Apr 2000 00:00:00 +0200Mechanization of Strong Kleene Logic for Partial Functions
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/359
Even though it is not very often admitted, partial functions do play asignificant role in many practical applications of deduction systems. Kleenehas already given a semantic account of partial functions using three-valuedlogic decades ago, but there has not been a satisfactory mechanization. Recentyears have seen a thorough investigation of the framework of many-valuedtruth-functional logics. However, strong Kleene logic, where quantificationis restricted and therefore not truth-functional, does not fit the frameworkdirectly. We solve this problem by applying recent methods from sorted logics.This paper presents a resolution calculus that combines the proper treatmentof partial functions with the efficiency of sorted calculi.Manfred Kerber; Michael Kohlhasepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/359Mon, 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 +0200Proving Ground Completeness of Resolution by Proof Planning
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/391
A lot of the human ability to prove hard mathematical theorems can be ascribedto a problem-specific problem solving know-how. Such knowledge is intrinsicallyincomplete. In order to prove related problems human mathematicians, however,can go beyond the acquired knowledge by adapting their know-how to new relatedproblems. These two aspects, having rich experience and extending it by need, can besimulated in a proof planning framework: the problem-specific reasoning knowledge isrepresented in form of declarative planning operators, called methods; since these aredeclarative, they can be mechanically adapted to new situations by so-called meta-methods. In this contribution we apply this framework to two prominent proofs intheorem proving, first, we present methods for proving the ground completeness ofbinary resolution, which essentially correspond to key lemmata, and then, we showhow these methods can be reused for the proof of the ground completeness of lockresolution.Manfred Kerber; Arthur C. Sehnpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/391Mon, 03 Apr 2000 00:00:00 +0200An Integration of Mechanised Reasoning and Computer Algebra that Respects Explicit Proofs
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/392
Mechanised reasoning systems and computer algebra systems have apparentlydifferent objectives. Their integration is, however, highly desirable, since in manyformal proofs both of the two different tasks, proving and calculating, have to beperformed. Even more importantly, proof and computation are often interwoven andnot easily separable. In the context of producing reliable proofs, the question howto ensure correctness when integrating a computer algebra system into a mechanisedreasoning system is crucial. In this contribution, we discuss the correctness prob-lems that arise from such an integration and advocate an approach in which thecalculations of the computer algebra system are checked at the calculus level of themechanised reasoning system. This can be achieved by adding a verbose mode to thecomputer algebra system which produces high-level protocol information that can beprocessed by an interface to derive proof plans. Such a proof plan in turn can beexpanded to proofs at different levels of abstraction, so the approach is well-suited forproducing a high-level verbalised explication as well as for a low-level machine check-able calculus-level proof. We present an implementation of our ideas and exemplifythem using an automatically solved extended example.Manfred Kerber; Michael Kohlhase; Volker Sorgepreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/392Mon, 03 Apr 2000 00:00:00 +0200Useful Properties of a Frame-Based Representation of Mathematical Knowledge
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/397
To prove difficult theorems in a mathematical field requires substantial know-ledge of that field. In this paper a frame-based knowledge representation formalismis presented, which supports a conceptual representation and to a large extent guar-antees the consistency of the built-up knowledge bases. We define a semantics ofthe representation by giving a translation into the underlaying logic.Manfred Kerberpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/397Mon, 03 Apr 2000 00:00:00 +0200A Mathematical Knowledge Base for Proving Theorems in Semigroup and Automata Theory
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/424
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.Barbara Schütt; Manfred Kerberpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/424Mon, 03 Apr 2000 00:00:00 +0200Omega: Towards a Mathematical Assistant
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/428
-mega is a mixed-initiative system with the ultimate pur-pose of supporting theorem proving in main-stream mathematics andmathematics education. The current system consists of a proof plannerand an integrated collection of tools for formulating problems, provingsubproblems, and proof presentation.Christoph Benzmüller; Lassaad Cheikhrouhou; Detlef Fehrer; Armin Fiedler; Xiaorong Huang; Manfred Kerber; Michael Kohlhase; Karsten Konrad; Andreas Meierpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/428Mon, 03 Apr 2000 00:00:00 +0200Adapting Methods to Novel Tasks in Proof Planning ?
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/255
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.Manfred Kerber; Xiaorong Huang; Michael Kohlhase; Jörn Richtsarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/255Mon, 03 Apr 2000 00:00:00 +0200Adapting the Diagonalization Method by Reformulations
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/257
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.Manfred Kerber; Xiaorong Huang; Lassaad Cheikhrouhouarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/257Mon, 03 Apr 2000 00:00:00 +0200A Tableau Calculus for Partial Functions
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/265
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.Michael Kohlhase; Manfred Kerberarticlehttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/265Mon, 03 Apr 2000 00:00:00 +0200