Exploiting the Addressee's Inferential Capabilities in Presenting Mathematical Proofs

Abstract

Proof presentation systems and, in some more general context, many natural language generation systems suffer from a crucial problem: they present too much information explicitly which the intended audience could more naturally infer from a less detailed text. Moreover, proofs in mathematical textbooks make extensive use of building chains of inferences in specialized notations, which is not sufficiently taken into account by proof presentation systems. Encouraged by these observations, we present a model for presenting mathematical proofs that (1) features the implicit conveyance of information through concise texts, (2) organizes major lines in the proof presentation around focused chains of inferences in a specialized notation, (3) can adapt its output to some of the capabilities of its audience. The methods described in this paper allow us to present proofs of moderately complex size in a quality approaching that of proofs found in mathematical textbooks.