Abstract
Unlike computer algebra systems, automated theorem provers have not yet achieved considerable recognition and relevance in mathematical practice. A significant shortcoming of mathematical proof assistance systems is that they require the fully formal representation of mathematical content, whereas in mathematical practice an informal, natural-language-like representation where obvious parts are omitted is common. We aim to support mathematical paper writing by integrating a scientific text editor and mathematical assistance systems such that mathematical derivations authored by human beings in a mathematical document can be automatically checked. To this end, we first define a calculus-independent representation language for formal mathematics that allows for underspecified parts. Then we provide two systems of rules that check if a proof is correct and at an acceptable level of granularity. These checks are done by decomposing the proof into basic steps that are then passed on to proof assistance systems for formal verification. We illustrate our approach using an example textbook proof.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abel, A., Chang, B.-Y.E., Pfenning, F.: Human-readable machine-verifiable proofs for teaching constructive logic. In: Egly, U., Fiedler, A., Horacek, H., Schmitt, S. (eds.) PROC of the Workshop on Proof Transformation, Proof Presentations and Complexity of Proofs (PTP 2001), pp. 37–50. Universitá degli studi di Siena (2001)
Autexier, S., Benzmüller, C., Fiedler, A., Lesourd, H.: Integrating proof assistants as reasoning and verification tools into a scientific WYSIWYG editor. In: Aspinall, D., Lüth, C. (eds.) User Interfaces for Theorem Provers (UITP 2005), pp. 16–39 (2005)
Bartle, R.G., Sherbert, D.: Introduction to Real Analysis, 2nd edn. Wiley, Chichester (1982)
de Bruijn, N.G.: The mathematical vernacular, a language for mathematics with typed sets. In: Nederpelt, et al. (eds.) [9], pp. 865–935.
Hilbert, D.: Die Grundlegung der elementaren Zahlenlehre. Mathematische Annalen 104, 485–494 (1930)
Huang, X.: Human Oriented Proof Presentation: A Reconstructive Approach, Infix, Sankt Augustin, Germany. DISKI, vol. 112 (1996)
Kamareddine, F., Maarek, M., Wells, J.: MathLang: An experience driven language of mathematics. Electronic Notes in Theoretical Computer Science 93C, 138–160 (2004)
Kamareddine, F., Nederpelt, R.: A refinement of de Bruijn’s formal language of mathematics. Logic, Language and Information 13(3), 287–340 (2004)
Nederpelt, R.P., Geuvers, J.H., de Vrijer, R.C. (eds.): Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, vol. 133. Elsevier, Amsterdam (1994)
Nederpelt, R.: Weak Type Theory: A formal language for mathematics. Computing Science Report 02-05, Eindhoven University of Technology, Department of Math. and Comp. Sc. (May 2002)
Nipkow, T.: Structured Proofs in Isar/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 259–278. Springer, Heidelberg (2003)
Ranta, A.: Grammatical framework — a type-theoretical grammar formalism. Journal of Functional Programming 14(2), 145–189 (2004)
Siekmann, J.H., Brezhnev, V., Cheikhrouhou, L., Fiedler, A., Horacek, H., Kohlhase, M., Meier, A., Melis, E., Moschner, M., Normann, I., Pollet, M., Sorge, V., Ullrich, C., Wirth, C.-P.: Proof development with ΩMEGA. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 144–149. Springer, Heidelberg (2002)
Wenzel, M., Wiedijk, F.: A comparison of the mathematical proof languages Mizar and Isar. Journal of Automated Reasoning 29, 389–411 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Autexier, S., Fiedler, A. (2006). Textbook Proofs Meet Formal Logic – The Problem of Underspecification and Granularity. In: Kohlhase, M. (eds) Mathematical Knowledge Management. MKM 2005. Lecture Notes in Computer Science(), vol 3863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11618027_7
Download citation
DOI: https://doi.org/10.1007/11618027_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31430-1
Online ISBN: 978-3-540-31431-8
eBook Packages: Computer ScienceComputer Science (R0)