A Human Oriented Proof Presentation Method

Abstract

It has long become a general consensus in the field of natural language generation that the whole generation task can be divided into two relatively independent parts: a so called text planner that decides on "what to say" and a generator that decides on "how to say it". This paper describes a text planner that decides on "what to say", currently under development at the University of Kaiserslautern for our automated theorem prover MKRP. The most important observation of this paper is, that the transformation task of this planner is primarily neither a linguistic problem nor a purely logical problem in the traditional sense: the transformation steps presented in this paper are based on a mental model of human proof presentation and our main effort was to make this model cognitively adequate. The model of human presentation consists primarily of the following three parts: 1. The identification of the size of human mathematical reasoning steps. The main observation is that human style inference steps usually have the "size" of at least an application of an axiom or a theorem. An algorithm is developed to generate domain-specific compound inference rules from axioms and theorems, which are then used to raise proofs to the so called conceptual level . 2. The ordering or "linearization" of proof parts: besides the logical constraint that proof lines must be first proved before they can be used, other pragmatic constraints on the ordering used in the "natural" human proof presentation are identified. In addition, a focus mechanism developed for natural language discourse is adapted and integrated to provide a total order. 3. Reference choices for each step: after the ordering each proof step will be translated into one message unit, which corresponds roughly to a sentence in the output text. Therefore, for each step we must decide how to refer to the used inference rules and the proof lines used as premises for this step, which parts to mention explicitly, implicitly and which ones to omit. A proof unit model is designed to attack this problem.