The Methods of Improving and Reorganizing Natural Deduction Proofs
Karol Pąk
Abstract:
The interaction between a proof assistant system and its user
can be improved not only by developing new features of the front-end
applications, but also by offering the user enriched readability of the underlying
formal language. Encoding of new mathematics is greatly simplified if the user has access to more legible texts in the library of already
formalized theories. Although a rich language enables writing readable
texts, it does not mean that all texts produced by authors sufficiently exploit
the language's capabilities. It can be observed analyzing nontrivial
examples of natural deduction proofs, either declarative or procedural,
that authors tend to create deductions which are correct for computers,
but hardly readable for humans, as they believe that finding and removing
inessential reasoning fragments, or shortening the proofs is not so
important as long as the computer accepts the proof script. To resolve
this problem we created auxiliary applications to improve the quality of
formal texts and we present them in this article.