Karol Pąk - Improving legibility of natural deduction proofs is not trivial

lmcs:850 - Logical Methods in Computer Science, September 18, 2014, Volume 10, Issue 3 - https://doi.org/10.2168/LMCS-10(3:23)2014
Improving legibility of natural deduction proofs is not trivialArticle

Authors: Karol Pąk ORCID

    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.


    Volume: Volume 10, Issue 3
    Published on: September 18, 2014
    Imported on: March 26, 2013
    Keywords: Computer Science - Logic in Computer Science

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1188 times.
    This article's PDF has been downloaded 513 times.