# Improving legibility of natural deduction proofs is not trivial

Source: [Improving legibility of natural deduction proofs is not trivial](<https://www.sota2.com/research/paper/68fa61fb1e209131ce9f6d8a>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2025-10-28T13:56:30.585Z

Authors: Karol P\\k{a}k

Published: 2014-07-04T07:27:50.000Z

## Abstract

In formal proof checking environments such as Mizar it is not merely the validity of mathematical formulas that is evaluated in the process of adoption to the body of accepted formalizations, but also the readability of the proofs that witness validity. As in case of computer programs, such proof scripts may sometimes be more and sometimes be less readable. To better understand the notion of readability of formal proofs, and to assess and improve their readability, we propose in this paper a method of improving proof readability based on Behaghel's First Law of sentence structure. Our method maximizes the number of local references to the directly preceding statement in a proof linearisation. It is shown that our optimization method is NP-complete.

## Recorded benchmark results

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

## Original sources and implementation

[Original paper](<https://arxiv.org/abs/1407.1140>)

[PDF](<https://arxiv.org/pdf/1407.1140.pdf>)