Supporting the formal verification of mathematical texts. (English) Zbl 1107.68104
Summary: The formal verification of mathematical texts is one of the most interesting applications for computer systems. In fact, we argue that the expert language of mathematics is the natural choice for achieving efficient mathematician-machine interaction. Our empirical approach, the analysis of carefully authored textbook proofs, forces us to focus on the language and the reasoning pattern that mathematician use when presenting proofs to colleagues and students. Enabling a machine to understand and follow such language and argumentation is seen to be the key to usable and acceptable math assistant systems. In this paper, we first perform an analysis of three textbook proofs by hand; we then describe a computational framework that aims at mechanising such an analysis. The resulting proof-of-concept implementation is capable of processing simple textbook proofs and constitutes promising steps towards a natural mathematician-machine interface for proof development and verification.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
Software:
CLAM; Isar; Automath; Coq; Nuprl; Proof General; Isabelle/Isar; IsaPlanner; OTTER; Isabelle/HOL; Oyster; Lambda-Clam; Mizar; XBarnacleReferences:
| [1] | P.W. Abrahams, Machine verification of mathematical proofs, PhD thesis, MIT, 1963; P.W. Abrahams, Machine verification of mathematical proofs, PhD thesis, MIT, 1963 |
| [2] | Aspinall, D., Proof general: A generic tool for proof development, (Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 1785 (2000), Springer: Springer Berlin), 38-42 · Zbl 0971.68627 |
| [3] | Autexier, S.; Benzmüller, C.; Fiedler, A.; Horacek, H.; Quoc Vo, B., Assertion-level proof representation with under-specification, Proceedings of the Mathematical Knowledge Management Symposium. Proceedings of the Mathematical Knowledge Management Symposium, Electronic Notes in Theoretical Computer Science, 93, 5-23 (2004) · Zbl 1271.68207 |
| [4] | Barendregt, H., Towards an interactive mathematical proof language, (Kamareddine, F., Thirty-Five Years of Automath (2003), Kluwer: Kluwer Dordrecht), 25-36 · Zbl 1063.68088 |
| [5] | Benzmüller, C.; Cheikhrouhou, L.; Fehrer, D.; Fiedler, A.; Huang, X.; Kerber, M.; Kohlhase, M.; Konrad, K.; Melis, E.; Meier, A.; Schaarschmidt, W.; Siekmann, J.; Sorge, V., Omega: Towards a mathematical assistant, (Proceedings of the 14th Conference on Automated Deduction. Proceedings of the 14th Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 1249 (1997), Springer: Springer Berlin), 252-255 · Zbl 1430.68393 |
| [6] | C. Benzmüller, A. Fiedler, M. Gabsdil, H. Horacek, I. Kruijff-Korbayova, D. Tsovaltzi, B. Quoc Vo, M. Wolska, Language phenomena in tutorial dialogs on mathematical proofs, in: I. Kruijff-Korbayova, C. Kosny, (Eds.), Proceedings of the 7th Workshop on the Semantics and Pragmatics of Dialogue DiaBruck, 2003, pp. 165-166; C. Benzmüller, A. Fiedler, M. Gabsdil, H. Horacek, I. Kruijff-Korbayova, D. Tsovaltzi, B. Quoc Vo, M. Wolska, Language phenomena in tutorial dialogs on mathematical proofs, in: I. Kruijff-Korbayova, C. Kosny, (Eds.), Proceedings of the 7th Workshop on the Semantics and Pragmatics of Dialogue DiaBruck, 2003, pp. 165-166 |
| [7] | M. Buckley, C. Benzmüller, System description: A dialog manager supporting tutorial natural language dialogue on proofs, in: ETAPS Satellite Workshop on User Interfaces for Theorem Provers (UITP), 2005; M. Buckley, C. Benzmüller, System description: A dialog manager supporting tutorial natural language dialogue on proofs, in: ETAPS Satellite Workshop on User Interfaces for Theorem Provers (UITP), 2005 |
| [8] | Bundy, A., The use of explicit proof plans to guide inductive proofs, (Lusk, R.; Overbeek, R., Proceedings of the 9th Conference on Automated Deduction (1988), Springer: Springer Berlin), 111-120 · Zbl 0656.68106 |
| [9] | Bundy, A.; Stevens, A.; van Harmelen, F.; Ireland, A.; Smaill, A., Rippling: A heuristic for guiding inductive proofs, Artificial Intelligence, 62, 185-253 (1993) · Zbl 0789.68121 |
| [10] | Bundy, A.; van Harmelen, F.; Horn, C.; Smaill, A., The oyster-clam system, (Stickel, M. E., Proceedings of the 10th International Conference on Automated Deduction (1990), Springer: Springer Berlin), 647-648 · Zbl 1509.68299 |
| [11] | Constable, R. L., Implementing Mathematics with the Nuprl Proof Development System (1986), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ |
| [12] | de Bruijn, N. G., The mathematical language AUTOMATH, its usage, and some of its extensions, (Laudet, M.; etal., Symposium on Automatic Demonstration. Symposium on Automatic Demonstration, Lectures Notes in Mathematics, vol. 125 (1970), Springer: Springer Berlin), 29-61 · Zbl 0208.20101 |
| [13] | de Bruijn, N. G., Mathematics and computers, Nieuw Archief voor Wiskunde, 7, 169-195 (1989) · Zbl 0701.00040 |
| [14] | Dixon, L.; Fleuriot, J. D., IsaPlanner: A prototype proof planner in Isabelle, (Baader, F., Proceedings of CADE’03. Proceedings of CADE’03, Lecture Notes in Computer Science (2003), Springer: Springer Berlin), 279-283 |
| [15] | G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin Mohring, B. Werner, The Coq proof assistant, version 5.6 user’s guide, Technical Report, INRIA—Rocquencourt, 1991; G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin Mohring, B. Werner, The Coq proof assistant, version 5.6 user’s guide, Technical Report, INRIA—Rocquencourt, 1991 |
| [16] | G. Ferguson, J.F. Allen, Arguing about plans: Plan representation and reasoning for mixed initiative planning, in: Proceedings of the Second Conference on Artificial Intelligence Planning Systems (AIPS-94), 1994, pp. 43-48; G. Ferguson, J.F. Allen, Arguing about plans: Plan representation and reasoning for mixed initiative planning, in: Proceedings of the Second Conference on Artificial Intelligence Planning Systems (AIPS-94), 1994, pp. 43-48 |
| [17] | A. Fiedler, User-adaptive proof explanation, PhD thesis, University of the Saarland, 2001; A. Fiedler, User-adaptive proof explanation, PhD thesis, University of the Saarland, 2001 |
| [18] | A. Frank, H. Kamp, On context-dependence in modal constructions, in: Proceedings of SALT 7, 1997; A. Frank, H. Kamp, On context-dependence in modal constructions, in: Proceedings of SALT 7, 1997 |
| [19] | Hallgren, T.; Ranta, A., An extensible proof text editor, (Parigot, M.; Voronkov, A., Logic for Programming and Automated Reasoning (LPAR’2000). Logic for Programming and Automated Reasoning (LPAR’2000), Lecture Notes in Computer Science, vol. 1955 (2000), Springer: Springer Berlin), 70-84 · Zbl 0988.68586 |
| [20] | Hanna, G., Rigorous Proof in Mathematics Education, Curriculum Series (1983), The Ontario Institute for Studies in Education |
| [21] | Hardy, G. H.; Wright, E. M., An Introduction to the Theory of Numbers (1971), Oxford at the Clarendon Press |
| [22] | Holland-Minkley, A. M.; Barzilay, R.; Constable, R. L., Verbalization of high level formal proofs, (Proceedings of the Sixteenth National Conference on Artificial Intelligence (1999), AAAI Press: AAAI Press Menlo Park, CA), 277-284 |
| [23] | Ireland, A.; Bundy, A., Productive use of failure in inductive proof, J. Automat. Reason., 16, 1-2, 79-111 (1996) · Zbl 0847.68103 |
| [24] | Kamareddine, F.; Nederpelt, R., A refinement of de Bruijn’s formal language of mathematics, J. Logic Language Inform., 13, 287-340 (2004) · Zbl 1048.03011 |
| [25] | Kamp, H.; Reyle, U., From Discourse to Logic (1993), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht |
| [26] | Landau, E., Grundlagen der Analysis (1960), Chelsea Publishing Company |
| [27] | LeVeque, W. J., Elementary Theory of Numbers, Series in Introductory Mathematics (1965), Addison-Wesley: Addison-Wesley Reading, MA |
| [28] | H. Lowe, D. Duncan, XBarnacle: Making theorem provers more accessible, in: CADE-14, 1997; H. Lowe, D. Duncan, XBarnacle: Making theorem provers more accessible, in: CADE-14, 1997 |
| [29] | McCarthy, J., Computer programs for checking mathematical proofs, (Recursive Function Theory. Recursive Function Theory, Proceedings of Symposia in Pure Mathematics, vol. 5 (1962), American Mathematical Society: American Mathematical Society Providence, RI), 219-228 · Zbl 0143.40007 |
| [30] | W. McCune, Otter 3.0 users guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, IL, 1994; W. McCune, Otter 3.0 users guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, IL, 1994 |
| [31] | R. Nederpelt, Weak type theory: A formal language for mathematics, Technical Report 02-05, Dept. of Mathematics and Computer Science, Eindhoven University of Technology, Box 513, 5600 MB Eindhoven, The Netherlands, 2002; R. Nederpelt, Weak type theory: A formal language for mathematics, Technical Report 02-05, Dept. of Mathematics and Computer Science, Eindhoven University of Technology, Box 513, 5600 MB Eindhoven, The Netherlands, 2002 |
| [32] | (Nederpelt, R. P.; Geuvers, J. H.; de Vrijer, R. C., Selected Papers on Automath. Selected Papers on Automath, Studies in Logic and the Foundations of Mathematics, vol. 133 (1994), North-Holland: North-Holland Amsterdam) · Zbl 0822.03009 |
| [33] | Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL—A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer: Springer Berlin · Zbl 0994.68131 |
| [34] | J.D.C. Richardson, A. Smaill, I. Green, System description: Proof planning in higher-order logic with Lambda-Clam, in: C. Kirchner, H. Kirchner (Eds.), Proceedings of the 15th Conference on Automated Deduction, 1998, pp. 129-133; J.D.C. Richardson, A. Smaill, I. Green, System description: Proof planning in higher-order logic with Lambda-Clam, in: C. Kirchner, H. Kirchner (Eds.), Proceedings of the 15th Conference on Automated Deduction, 1998, pp. 129-133 |
| [35] | Roberts, C., Modal subordination and pronominal anaphora in discourse, Linguistics & Philosophy, 12, 683-721 (1989) |
| [36] | P. Rudnicki, An overview of the MIZAR project, Technical Report, Department of Computer Science, University of Alberta, Edmonton, 1992; P. Rudnicki, An overview of the MIZAR project, Technical Report, Department of Computer Science, University of Alberta, Edmonton, 1992 |
| [37] | Simon, D. L., Checking natural language proofs, (Lusk, E. L.; Overbeek, R. A., 9th International Conference on Automated Deduction. 9th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 310 (1988), Springer: Springer Berlin) · Zbl 0657.68099 |
| [38] | Trybulec, A., The MIZAR-QC/6000 logic information language, ALLC, 6, 136-140 (1978) |
| [39] | L.S. van Benthem Jutting, Checking Landau’s “Grundlagen” in the AUTOMATH system, PhD thesis, TH Eindhoven, 1977; L.S. van Benthem Jutting, Checking Landau’s “Grundlagen” in the AUTOMATH system, PhD thesis, TH Eindhoven, 1977 · Zbl 0402.68064 |
| [40] | van Eijck, J.; Kamp, H., Representing discourse in context, (van Benthem, J.; ter Meulen, A., Handbook of Logic & Language (1997), Elsevier Science B.V.: Elsevier Science B.V. Amsterdam), 179-237, Chapter 3 |
| [41] | Wang, H., Towards Mechanical Mathematics, IBM J. Res. Develop., 4, 1 (1960) · Zbl 0097.00404 |
| [42] | Webber, B.; Stone, M.; Joshi, A.; Knott, A., Anaphora and discourse structure, Computational Linguistics, 29, 4, 545-587 (2003) · Zbl 1234.91006 |
| [43] | Weidenbach, C., Combining superposition, sorts and splitting, (Robinson, J. A.; Voronkov, A., Handbook of Automated Reasoning, vol. 4 (2001), MIT Press: MIT Press Cambridge, MA) · Zbl 1011.68129 |
| [44] | Wenzel, M., Isar—a generic interpretative approach to readable formal proof documents, (Bertot, Y.; Dowek, G.; Hirschowitz, A.; Paulin, C.; Thery, L., Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99. Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, Lecture Notes in Computer Science, vol. 1690 (1999), Springer: Springer Berlin), 167-184 · Zbl 0929.00038 |
| [45] | M. Wenzel, Isabelle/Isar—a versatile environment for human-readable formal proof documents, PhD thesis, Institut für Informatik, TU München, 2002; M. Wenzel, Isabelle/Isar—a versatile environment for human-readable formal proof documents, PhD thesis, Institut für Informatik, TU München, 2002 |
| [46] | Wenzel, M.; Wiedijk, F., A comparison of the mathematical proof languages Mizar and Isar, J. Automat. Reason., 29, 3-4, 389-411 (2002) · Zbl 1064.68083 |
| [47] | C. Zinn, Understanding informal mathematical discourse, PhD thesis, Institut für Informatik, Universität Erlangen-Nürnberg, September 2004. Published as: Arbeitsberichte des Instituts für Informatik, Band 37, Nr. 4, ISSN 0344-3515; C. Zinn, Understanding informal mathematical discourse, PhD thesis, Institut für Informatik, Universität Erlangen-Nürnberg, September 2004. Published as: Arbeitsberichte des Instituts für Informatik, Band 37, Nr. 4, ISSN 0344-3515 · Zbl 1101.68836 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
