Refine
Keywords
- Declarative and Procedural Knowledge (1)
- Deduction (1)
- Methods (1)
- Planning and Verification (1)
- Tactics (1)
-
Adapting Methods to Novel Tasks in Proof Planning ?
(1999)
- 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.
-
Adapting the Diagonalization Method by Reformulations
(1999)
- 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.
-
Reconstructing Proofs at the Assertion Level
(1999)
- 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.
-
Planning Reference Choices for Argumentative Texts
(1999)
- 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.
-
Translating Machine-Generated Resolution Proofs into ND-Proofs at the Assertion Level
(1999)
- 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.
-
Planning Mathematical Proofs with Methods
(1999)
- In this article we formally describe a declarative approach for encoding plan operatorsin proof planning, the so-called methods. The notion of method evolves from the much studiedconcept tactic and was first used by Bundy. While significant deductive power has been achievedwith the planning approach towards automated deduction, the procedural character of the tacticpart of methods, however, hinders mechanical modification. Although the strength of a proofplanning system largely depends on powerful general procedures which solve a large class ofproblems, mechanical or even automated modification of methods is nevertheless necessary forat least two reasons. Firstly methods designed for a specific type of problem will never begeneral enough. For instance, it is very difficult to encode a general method which solves allproblems a human mathematician might intuitively consider as a case of homomorphy. Secondlythe cognitive ability of adapting existing methods to suit novel situations is a fundamentalpart of human mathematical competence. We believe it is extremely valuable to accountcomputationally for this kind of reasoning.The main part of this article is devoted to a declarative language for encoding methods,composed of a tactic and a specification. The major feature of our approach is that the tacticpart of a method is split into a declarative and a procedural part in order to enable a tractableadaption of methods. The applicability of a method in a planning situation is formulatedin the specification, essentially consisting of an object level formula schema and a meta-levelformula of a declarative constraint language. After setting up our general framework, wemainly concentrate on this constraint language. Furthermore we illustrate how our methodscan be used in a Strips-like planning framework. Finally we briefly illustrate the mechanicalmodification of declaratively encoded methods by so-called meta-methods.
-
Presenting Machine-Found Proofs
(1999)
- This paper outlines an implemented system named PROVERBthat transforms and abstracts machine-found proofs to natural deduction style proofs at an adequate level of abstraction and then verbalizesthem in natural language. The abstracted proofs, originally employedonly as an intermediate representation, also prove to be useful for proofplanning and proving by analogy.
