Refine
Keywords
- Declarative and Procedural Knowledge (1)
- Deduction (1)
- Methods (1)
- Planning and Verification (1)
- Tactics (1)
-
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.
-
Generating Multilingual Proofs
(1999)
- This paper outlines the microplanner of PROVERB , a system that generates multilingual text from machine-found mathematical proofs. The main representational vehicle is the text structure proposed by Meteer. Following Panaget, we also distinguish between the ideational and the textual semantic categories, and use the upper model to replace the former. Based on this, a further extension is made to support aggregation before realization decisions are made. While our the framework of our macroplanner is kept languageindependent, our microplanner draws on language specific linguistic sources such as realization classes and lexicon. Since English and German are the first two languages to be generated and because the sublanguage of our mathematical domain is relatively limited, the upper model and the textual semantic categories are designed to cope with both languages. Since the work reported is still in progress, we also discuss open problems we are facing.
-
Proof Verbalization as an Application of NLG
(1999)
- This paper describes the linguistic part of a system called PROVERB, which transforms, abstracts,and verbalizes machine-found proofs into formatedtexts. Linguistically, the architecture of PROVERB follows most application oriented systems, and is a pipelined control of three components. Its macroplanner linearizes a proof and plans mediating communicative acts by employing a combination of hierarchical planning and focus-guided navigation. The microplanner then maps communicative acts and domain concepts into linguistic resources, paraphrases and aggregates such resources to producethe final Text Structure. A Text Structure contains all necessary syntactic information, and can be executed by our realizer into grammatical sentences. The system works fully automatically and performs particularly well for textbook size examples.
-
Proof Verbalization in PROVERB
(1999)
- This paper outlines the linguistic part of an implemented system namedPROVERB[3] that transforms, abstracts, and verbalizes machine-found proofs innatural language. It aims to illustrate, that state-of-the-art techniques of natural language processing are necessary to produce coherent texts that resemble those found in typical mathematical textbooks, in contrast to the belief that mathematical texts are only schematic and mechanical.The verbalization module consists of a content planner, a sentence planner, and a syntactic generator. Intuitively speaking, the content planner first decides the order in which proof steps should be conveyed. It also some messages to highlight global proof structures. Subsequently, thesentence planner combines and rearranges linguistic resources associated with messages produced by the content planner in order to produce connected text. The syntactic generat or finally produces the surface text.
-
Reuse of Proofs by Meta-Methods
(1999)
- 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.
-
Die Beweisentwicklungsumgebung Omega-MKRK
(1999)
- 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.
