×

On correctness of mathematical texts from a logical and practical point of view. (English) Zbl 1166.68353

Autexier, Serge (ed.) et al., Intelligent computer mathematics. 9th international conference, AISC 2008, 15th symposium, Calculemus 2008, 7th international conference, MKM 2008, Birmingham, UK, July 28–August 1, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85109-7/pbk). Lecture Notes in Computer Science 5144. Lecture Notes in Artificial Intelligence, 583-598 (2008).
Summary: Formalizing mathematical argument is a fascinating activity in itself and (we hope!) also bears important practical applications. While traditional proof theory investigates deducibility of an individual statement from a collection of premises, a mathematical proof, with its structure and continuity, can hardly be presented as a single sequent or a set of logical formulas. What is called “mathematical text”, as used in mathematical practice through the ages, seems to be more appropriate. However, no commonly adopted formal notion of mathematical text has emerged so far.
In this paper, we propose a formalism which aims to reflect natural (human) style and structure of mathematical argument, yet to be appropriate for automated processing: principally, verification of its correctness (we consciously use the word rather than “soundness” or “validity”).
We consider mathematical texts that are formalized in the ForTheL language (brief description of which is also given) and we formulate a point of view on what a correct mathematical text might be. Logical notion of correctness is formalized with the help of a calculus. Practically, these ideas, methods and algorithms are implemented in a proof assistant called SAD. We give a short description of SAD and a series of examples showing what can be done with it.
For the entire collection see [Zbl 1154.68002].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68U15 Computing methodologies for text processing; mathematical typography
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Wang, H., Towards mechanical mathematics, IBM J. of Research and Development, 4, 2-22 (1960) · Zbl 0097.00404 · doi:10.1147/rd.41.0002
[2] Glushkov, V. M., Some problems of automata theory and artificial intelligence (in Russian), Kibernetika, 2, 3-13 (1970) · Zbl 0242.68056
[3] Lyaletski, A.; Paskevich, A.; Verchinine, K.; Asperti, A.; Bancerek, G.; Trybulec, A., Theorem proving and proof verification in the system SAD, Mathematical Knowledge Management, 236-250 (2004), Heidelberg: Springer, Heidelberg · Zbl 1108.68573
[4] Lyaletski, A.; Paskevich, A.; Verchinine, K., SAD as a mathematical assistant — how should we go from here to there?, Journal of Applied Logic, 4, 4, 560-591 (2006) · Zbl 1107.68099 · doi:10.1016/j.jal.2005.10.009
[5] Verchinine, K.; Lyaletski, A.; Paskevich, A.; Pfenning, F., System for Automated Deduction (SAD): a tool for proof verification, Automated Deduction - CADE-21, 398-403 (2007), Heidelberg: Springer, Heidelberg · Zbl 1213.68576 · doi:10.1007/978-3-540-73595-3_29
[6] Wiedijk, F., The Seventeen Provers of the World (2006), Heidelberg: Springer, Heidelberg
[7] Bertot, Y.; Castéran, P., Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions (2004), Heidelberg: Springer, Heidelberg · Zbl 1069.68095
[8] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002), Heidelberg: Springer, Heidelberg · Zbl 0994.68131
[9] Owre, S.; Rushby, J. M.; Shankar, N.; Kapur, D., PVS: a prototype verification system, Automated Deduction - CADE-11, 748-752 (1992), Heidelberg: Springer, Heidelberg
[10] Gordon, M. J.C.; Melham, T. F., Introduction to HOL: a theorem proving environment for higher order logic (1993), Cambridge: Cambridge University Press, Cambridge · Zbl 0779.68007
[11] Nederpelt, R. P.; Geuvers, J. H.; de Vrijer, R. C., Selected Papers on Automath (1994), Amsterdam: North-Holland, Amsterdam · Zbl 0822.03009
[12] Trybulec, A.; Blair, H., Computer assisted reasoning with Mizar, Proc. 9th International Joint Conference on Artificial Intelligence, 26-28 (1985), San Francisco: Morgan Kaufmann, San Francisco
[13] Wenzel, M.; Bertot, Y.; Dowek, G.; Hirschowitz, A.; Paulin, C.; Théry, L., Isar — a generic interpretative approach to readable formal proof documents, Theorem Proving in Higher Order Logics, 167-184 (1999), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-48256-3_12
[14] Kamareddine, F.; Nederpelt, R. P., A Refinement of de Bruijn’s Formal Language of Mathematics, Journal of Logic, Language and Information, 13, 3, 287-340 (2004) · Zbl 1048.03011 · doi:10.1023/B:JLLI.0000028393.47593.b8
[15] Jojgov, G.; Nederpelt, R.; Asperti, A.; Bancerek, G.; Trybulec, A., A path to faithful formalizations of mathematics, Mathematical Knowledge Management, 145-159 (2004), Heidelberg: Springer, Heidelberg · Zbl 1108.68591
[16] Kamareddine, F.; Maarek, M.; Wells, J. B.; Asperti, A.; Bancerek, G.; Trybulec, A., Flexible encoding of mathematics on the computer, Mathematical Knowledge Management, 145-159 (2004), Heidelberg: Springer, Heidelberg
[17] Kaufmann, M.; Manolios, P.; Moore, J. S., Computer-Aided Reasoning: An Approach (2000), Dordrecht: Kluwer, Dordrecht
[18] Richardson, J.; Smaill, A.; Green, I.; Kirchner, C.; Kirchner, H., System description: Proof planning in higher-order logic with Lambda-Clam, Automated Deduction - CADE-15, 129-133 (1998), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0054254
[19] Buchberger, B.; Crăciun, A.; Jebelean, T.; Kovács, L.; Kutsia, T.; Nakagawa, K.; Piroi, F.; Popov, N.; Robu, J.; Rosenkranz, M.; Windsteiger, W., Theorema: Towards computer-aided mathematical theory exploration, Journal of Applied Logic, 4, 4, 470-504 (2006) · Zbl 1107.68095 · doi:10.1016/j.jal.2005.10.006
[20] Vershinin, K.; Paskevich, A., ForTheL — the language of formal theories, International Journal of Information Theories and Applications, 7, 3, 120-126 (2000)
[21] Paskevich, A., Verchinine, K., Lyaletski, A., Anisimov, A.: Reasoning inside a formula and ontological correctness of a formal mathematical text. In: Calculemus/MKM 2007 — Work in Progress, University of Linz, Austria. Number 07-06 in RISC-Linz Report Series, pp. 77-91 (2007)
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.