Refine
Year of publication
- 1999 (15) (remove)
Document Type
- Preprint (15) (remove)
Language
- English (15) (remove)
Has Fulltext
- yes (15)
Keywords
- Case-Based Reasoning (2)
- EBG (1)
- Fallbasiertes Schliessen (1)
- Fallbasiertes Schließen (1)
- Similarity Assessment (1)
- analogy (1)
- case-based reasoning (1)
- concept representation (1)
- problem solving (1)
- typical examples (1)
Faculty / Organisational entity
Planning means constructing a course of actions to achieve a specified set of goals when starting from an initial situation. For example, determining a sequence of actions (a plan) for transporting goods from an initial location to some destination is a typical planning problem in the transportation domain. Many planning problems are of practical interest.
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)
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.
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.
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 recent years several computational systems and techniques fortheorem proving by analogy have been developed. The obvious prac-tical question, however, as to whether and when to use analogy hasbeen neglected badly in these developments. This paper addresses thisquestion, identifies situations where analogy is useful, and discussesthe merits of theorem proving by analogy in these situations. Theresults can be generalized to other domains.
Constructing an analogy between a known and already proven theorem(the base case) and another yet to be proven theorem (the target case) oftenamounts to finding the appropriate representation at which the base and thetarget are similar. This is a well-known fact in mathematics, and it was cor-roborated by our empirical study of a mathematical textbook, which showedthat a reformulation of the representation of a theorem and its proof is in-deed more often than not a necessary prerequisite for an analogical inference.Thus machine supported reformulation becomes an important component ofautomated analogy-driven theorem proving too.The reformulation component proposed in this paper is embedded into aproof plan methodology based on methods and meta-methods, where the latterare used to change and appropriately adapt the methods. A theorem and itsproof are both represented as a method and then reformulated by the set ofmetamethods presented in this paper.Our approach supports analogy-driven theorem proving at various levels ofabstraction and in principle makes it independent of the given and often acci-dental representation of the given theorems. Different methods can representfully instantiated proofs, subproofs, or general proof methods, and hence ourapproach also supports these three kinds of analogy respectively. By attachingappropriate justifications to meta-methods the analogical inference can oftenbe justified in the sense of Russell.This paper presents a model of analogy-driven proof plan construction andfocuses on empirically extracted meta-methods. It classifies and formally de-scribes these meta-methods and shows how to use them for an appropriatereformulation in automated analogy-driven theorem proving.
This case study examines in detail the theorems and proofs that are shownby analogy in a mathematical textbook on semigroups and automata, thatis widely used as an undergraduate textbook in theoretical computer scienceat German universities (P. Deussen, Halbgruppen und Automaten, Springer1971). The study shows the important role of restructuring a proof for findinganalogous subproofs, and of reformulating a proof for the analogical trans-formation. It also emphasizes the importance of the relevant assumptions ofa known proof, i.e., of those assumptions actually used in the proof. In thisdocument we show the theorems, the proof structure, the subproblems andthe proofs of subproblems and their analogues with the purpose to providean empirical test set of cases for automated analogy-driven theorem proving.Theorems and their proofs are given in natural language augmented by theusual set of mathematical symbols in the studied textbook. As a first step weencode the theorems in logic and show the actual restructuring. Secondly, wecode the proofs in a Natural Deduction calculus such that a formal analysisbecomes possible and mention reformulations that are necessary in order toreveal the analogy.
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.