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 +0200Aggregation in the Generation of Argumentative Texts
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/215
Armin Fiedler; Xiaorong Huangpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/215Mon, 03 Apr 2000 00:00:00 +0200Mikroplanungstechniken zur Präsentation mathematischer Beweise
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/226
Armin Fiedlermasterthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/226Mon, 03 Apr 2000 00:00:00 +0200Presenting Machine-Found Proofs
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/237
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.Armin Fiedler; Xiaorong Huangpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/237Mon, 03 Apr 2000 00:00:00 +0200Generating Multilingual Proofs
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/247
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.Armin Fiedler; Xiaorong Huangpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/247Mon, 03 Apr 2000 00:00:00 +0200Proof Verbalization as an Application of NLG
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/248
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.Armin Fiedler; Xiaorong Huangpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/248Mon, 03 Apr 2000 00:00:00 +0200Proof Verbalization in PROVERB
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/249
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.Armin Fiedler; Xiaorong Huangpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/249Mon, 03 Apr 2000 00:00:00 +0200Paraphrasing and Aggregating Argumentative Text Using Text Structure
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/256
We argue in this paper that sophisticated mi-croplanning techniques are required even formathematical proofs, in contrast to the beliefthat mathematical texts are only schematicand mechanical. We demonstrate why para-phrasing and aggregation significantly en-hance the flexibility and the coherence ofthe text produced. To this end, we adoptedthe Text Structure of Meteer as our basicrepresentation. The type checking mecha-nism of Text Structure allows us to achieveparaphrasing by building comparable combi-nations of linguistic resources. Specified interms of concepts in an uniform ontologicalstructure called the Upper Model, our se-mantic aggregation rules are more compactthan similar rules reported in the literature.Armin Fiedler; Xiaorong Huangpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/256Mon, 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 +0200