Abstract
Proof development in proof assistants such as HOL, Coq, Mizar, etc. is an activity where authors usually produce proofs by typing out proof scripts or system tactics. Quite frequently, however, authors also have to read existing proof scripts, either to imitate smart proof pieces, or to refactor fragments of reasoning to make some theorem stronger, more easily applicable and so on. Therefore, it is important to develop techniques to improve legibility of proofs, since it directly affects productivity of script writers. To analyze the legibility of natural deduction proofs, we investigate proof graphs that represent the flow of information in given reasoning. Our analysis of the information flow leads to methods of improving proof readability based on Behaghel’s First Law, which states that in legible text relevant pieces of information must occur close to each other. The presented method maximizes the number of close connections between premises and steps that use these steps as justification. In this paper we show that our optimization method is NP-hard.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar Mathematical Library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Proceedings of the 18th Calculemus and 10th International Conference on Intelligent Computer Mathematics Lecture Notes in Computer Science, vol. 6824, pp 149–163. Springer-Verlag , Berlin, Heidelberg (2011)
Bancerek, G.: The fundamental properties of natural numbers. Formalized Math. 1(1), 41–46 (1990)
Behaghel, O.: Beziehungen zwischen Umfang und Reihenfolge von Satzgliedern. Indogermanische Forschungen 25, 110–142 (1909)
Corbineau, P.: A Declarative Language for the Coq Proof Assistant. In: Proceedings of the 2007 International Conference on Types for Proofs and Programs, pp 69–84 (2007)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. A Series of Books in the Mathematical Science. W. H. Freeman and Company, New York (1979)
Giero, M., Wiedijk, F.: MMode, A Mizar Mode for the proof assistant Coq. Technical report, ICIS. Radboud Universiteit Nijmegen (2004)
Gonthier, G.: Formal Proof—The Four-Color Theorem. Notices of the AMS 55 (11), 1382–1393 (2008)
Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a Nutshell. J. Formalized Reason. 3(2), 153–245 (2010)
Grabowski, A., Schwarzweller, C.: Translating mathematical vernacular into knowledge repositories. In: Proceedings of the 4th international conference on Mathematical Knowledge Management MKM’05, pp 49–64. Springer-Verlag, Berlin, Heidelberg (2006)
Grabowski, A., Schwarzweller, C.: Revisions as an Essential Tool to Maintain Mathematical Repositories. In: Proceedings of the 14th symposium on Towards Mechanized Mathematical Assistants: 6th International Conference, Lecture Notes in Computer Science, vol. 4573, pp 235–249. Springer-Verlag (2007)
Grabowski, A.: Automated discovery of properties of rough sets. Fundamenta Informaticae 128(1-2), 65–79 (2013)
Grabowski, A.: Efficient rough set theory merging. Fundamenta Informaticae 135(4), 371–385 (2014)
Grabowski, A., Jastrzębska, M.: A note on a formal approach to rough operators. In: Szczuka, M.S., Kryszkiewicz, M., Ramanna, S., Jensen, R., Hu, Q. (eds.) Rough Sets and Current Trends in Computing - 7th International Conference, RSCTC 2010, Warsaw, Poland, June 28-30,2010. Proceedings, volume 6086 of Lecture Notes in Computer Science, pp 307–316. Springer (2010)
Grabowski, A., Schwarzweller, C.: Towards automatically categorizing mathematical knowledge. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Federated Conference on Computer Science and Information Systems – FedCSIS 2012, Wroclaw, Poland, 9–12 September 2012, Proceedings, pp 63–68 (2012)
Harrison, J.: A Mizar Mode for HOL. In: Proc. of the 9th International Conference on Theorem Proving in Higher Order Logics, pp 203–220. Springer (1996)
Korniłowicz, A.: Tentative Experiments with Ellipsis in Mizar. In: Intelligent Computer Mathematics Lecture Notes in Computer Science, vol. 7362, pp 453–457 (2012)
Korniłowicz, A.: On Rewriting Rules in Mizar. J. Autom. Reason. 50(2), 203–210 (2013)
Lawler, E.L.: Combinatorial Optymization: Networks and Matroids. Holt, Rinehart and Winston (1967)
Naumowicz, A., Bylinski, C.: Improving MIZAR texts with properties and requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) Third International Conference Mathematical Knowledge Management 2004, MKM’04 Lecture Notes in Computer Science, vol. 3119, pp 290–301. Springer-Verlag (2004)
Naumowicz, A., Kornilowicz, A.: A Brief Overview of Mizar. In: TPHOLs’09, Lecture Notes in Computer Science, vol. 5674, pp 67–72. Springer-Verlag (2009)
Naumowicz, A.: Interfacing external CA systems for Grobner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1–11 (2010)
Pak, K.: The algorithms for improving and reorganizing natural deduction proofs. Stud. Logic Grammar Rhetoric 22(35), 95–112 (2010)
Pak, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217–228 (2013)
Pak, K.: Improving legibility of natural deduction proofs is not trivial. Logical Methods in Computer Science 10(3:23), 1–30 (2014)
Syme, D.: Three Tactic Theorem Proving. In: Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 1690, pp 203–220. Springer-Verlag (1999)
Trybulec, A., Kornilowicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. J. Autom. Reason. 50(2), 119–121 (2013)
Urban, J.: XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. In: Bonacina, M.P. (ed.) 4th International Conference Mathematical Knowledge Management 2005, MKM’05 volume 3863 of Lecture Notes in Computer Science, pp 346–360. Springer-Verlag (2005)
Wenzel, M.: The Isabelle/Isar Reference Manual. University of Cambridge (2011)
Wiedijk, F.: Mizar Light for HOL Light. In: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, pp 378–394 (2001)
Author information
Authors and Affiliations
Corresponding author
Additional information
The paper has been financed by the resources of the Polish National Science Centre granted by decision no DEC-2012/07/N/ST6/02147
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Pąk, K. Improving Legibility of Formal Proofs Based on the Close Reference Principle is NP-Hard. J Autom Reasoning 55, 295–306 (2015). https://doi.org/10.1007/s10817-015-9337-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-015-9337-1