Abstract
Both easily readable and obscure proof scripts can be found in the bodies of formalisations around formal proof checking environments such as Mizar. The communities that use this system try to encourage writing legible texts by making available various solutions, e.g., by introduction of phrases and constructs that make formal deductions look closer to the informal ones. Still, many authors do not want to invest additional efforts in enhancing readability of their scripts and assume this can be handled automatically for them. Therefore, it is desirable to create a tool that can automatically improve legibility of proofs. It turns out that this goal is non-trivial since improving features of text that enhance legibility is in general NP-complete.
The successful application of SMT technology to solving computationally difficult problems suggests that available SMT solvers can give progress in legibility enhancement. In this paper we present the first experimental results obtained with automated legibility improving tools for the Mizar system that use Z3 solver in the backend.
The paper has been financed by the resources of the Polish National Science Center granted by decision n°DEC-2012/07/N/ST6/02147.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Behaghel, O.: Beziehungen zwischen Umfang und Reihenfolge von Satzgliedern. Indogermanische Forschungen 25, 110–142 (1909)
Blanchette, J.C.: Redirecting Proofs by Contradiction. In: Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013. EPiC Series, vol. 14, pp. 11–26. EasyChair (2013)
Cowan, N.: The magical number 4 in short-term memory: A reconsideration of mental storage capacity. Behavioral and Brain Sciences 24(1), 87–114 (2001)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Ericsson, K.A.: Analysis of memory performance in terms of memory skill. Advances in the psychology of human intelligence, vol. 4. Lawrence Erlbaum Associates Inc., Hillsdale (1988)
Fitch, F.B.: Symbolic Logic: an Introduction. The Ronald Press Co. (1952)
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)
Gonthier, G.: Formal Proof—The Four-Color Theorem. Notices of the AMS 55(11), 1382–1393 (2008)
Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a Nutshell. Journal of Formalized Reasoning 3(2), 153–245 (2010)
Grabowski, A., Schwarzweller, C.: Improving Representation of Knowledge within the Mizar Library. Studies in Logic, Grammar and Rhetoric 18(31), 35–50 (2009)
Jaśkowski, S.: On the Rules of Supposition in Formal Logic. Studia Logica (1934), Warszawa Reprinted in Polish Logic, McCall, S., ed. Clarendon Press, Oxford (1967)
Kaliszyk, C., Urban, J.: PRocH: Proof Reconstruction for HOL Light. In: Bonacina, M.P. (ed.) CADE-24. LNCS (LNAI), vol. 7898, pp. 267–274. Springer, Heidelberg (2013)
Ko, A.J., Myers, B.A., Coblenz, M.J., Aung, H.H.: An Exploratory Study of How Developers Seek, Relate, and Collect Relevant Information during Software Maintenance Tasks. IEEE Transactions on Software Engineering 32(12), 971–988 (2006)
Korniłowicz, A.: Tentative Experiments with Ellipsis in Mizar. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 453–457. Springer, Heidelberg (2012)
Levy, R.: Expectation-based syntactic comprehension. Cognition 106, 1126–1177 (2008)
Matuszewski, R.: On Automatic Translation of Texts from Mizar-QC language into English. Studies in Logic, Grammar and Rhetoric 4 (1984)
Miller, G.A.: The Magical Number Seven, Plus or Minus Two: Some Limits on Our Capacity for Processing Information. Psychological Review 63, 81–97 (1956)
Naumowicz, A., Korniłowicz, A.: A Brief Overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67–72. Springer, Heidelberg (2009)
Naumowicz, A., Korniłowicz, A.: A Brief Overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67–72. Springer, Heidelberg (2009)
Pąk, K.: The Algorithms for Improving and Reorganizing Natural Deduction Proofs. Studies in Logic, Grammar and Rhetoric 22(35), 95–112 (2010)
Pąk, K.: Methods of Lemma Extraction in Natural Deduction Proofs. Journal of Automated Reasoning 50(2), 217–228 (2013)
Pąk, K.: The Algorithms for Improving Legibility of Natural Deduction Proofs. PhD thesis, University of Warsaw (2013)
Pąk, K., Trybulec, A.: Laplace Expansion. Formalized Mathematics 15(3), 143–150 (2008)
Smolka, S.J., Blanchette, J.C.: Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. In: Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013. EPiC Series, vol. 14, pp. 117–132. EasyChair (2013)
Urban, J.: XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 346–360. Springer, Heidelberg (2006)
Urban, J.: MizarMode - An Integrated Proof Assistance Tool for the Mizar Way of Formalizing Mathematics. Journal of Applied Logic 4(4), 414–427 (2006)
Wenzel, M.: The Isabelle/Isar Reference Manual. University of Cambridge (2011)
Whitehead, A.N., Russell, B.: Principia Mathematica to *56. Cambridge Mathematical Library. Cambridge University Press (1910)
Zammit, V.: On the Readability of Machine Checkable Formal Proofs. PhD thesis, The University of Kent at Canterbury (March 1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Pąk, K. (2014). Automated Improving of Proof Legibility in the Mizar System. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds) Intelligent Computer Mathematics. CICM 2014. Lecture Notes in Computer Science(), vol 8543. Springer, Cham. https://doi.org/10.1007/978-3-319-08434-3_27
Download citation
DOI: https://doi.org/10.1007/978-3-319-08434-3_27
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08433-6
Online ISBN: 978-3-319-08434-3
eBook Packages: Computer ScienceComputer Science (R0)