Presenting machine-generated proofs in terms adequate to the needs of a human audience is a serious challenge. One salient property of mathematical proofs as typically found in textbooks is that lines of reasoning are expressed in a rather condensed form by leaving out elementary and easily inferable, but logically necessary inference steps, while explaining involved ones in more detail. To date, automated proof presentation techniques are not able to deal with this issue in an adequate manner. Addressing this problem in a principled way, we describe an approach that successively enhances a logically self-contained proof at the assertion level through communicatively justified modifications of the original line of reasoning. These enhancements include expansion of involved theorem applications, omission of trivial justifications, compactification of intermediate inference steps, and broadening the scope of justifications to support focused argumentation, as in chains of inequations. Through incorporating these measurements, many proofs are presented in a shorter and better understandable fashion than in previous approaches.
展开▼
