Improving legibility of natural deduction proofs is not trivial
Improving legibility of natural deduction proofs is not trivial
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 …