Abstract
Despite great advances in computer-assisted proof systems, writing formal proofs using a traditional computer is still challenging due to mouse-and-keyboard interaction. This leads to scientists often resorting to pen and paper to write their proofs. However, when handwriting a proof, there is no formal guarantee that the proof is correct. In this paper we address this issue and present the initial steps towards a system that allows users to handwrite proofs using a pen-based device and that communicates with an external theorem prover to support the users throughout the proof writing process. We focus on calculational proofs, whereby a theorem is proved by a chain of formulae, each transformed in some way into the next. We present the implementation of a proof-of-concept prototype that can formally verify handwritten calculational proofs without the need to learn the specific syntax of theorem provers.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Anderson, R., Anderson, R., Chung, O., Davis, K.M., Davis, P., Prince, C., Razmov, V., Simon, B.: Classroom presenter - a classroom interaction system for active and collaborative learning. In: WIPTE (2006)
Aspinall, D.: Proof general: a generic tool for proof development. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 38–43. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_3
Backhouse, R.: The calculational method. Inf. Process. Lett. 53(3), 121 (1995)
Backhouse, R., Ferreira, J.F.: On Euclid’s algorithm and elementary number theory. Sci. Comput. Program. 76(3), 160–180 (2011). https://doi.org/10.1016/j.scico.2010.05.006. http://joaoff.com/publications/2010/euclid-alg
Backhouse, R., Michaelis, D.: Exercises in quantifier manipulation. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 69–81. Springer, Heidelberg (2006). https://doi.org/10.1007/11783596_7
Backhouse, R., Verhoeven, R.: \({\sf Math }\!\!\int \!\!{\sf pad}\): a system for on-line preparation of mathematical documents. Softw. Concepts Tools 18, 80–89 (1997)
Bauer, G., Wenzel, M.: Calculational reasoning revisited an Isabelle/Isar experience. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 75–90. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44755-5_7
Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-662-07964-5
Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, New York (1990). https://doi.org/10.1007/978-1-4612-3228-5
Ferreira, J.F., Mendes, A.: Students’ feedback on teaching mathematics through the calculational method. In: 39th ASEE/IEEE Frontiers in Education Conference. IEEE (2009)
Ferreira, J.F., Mendes, A.: A calculational approach to path-based properties of the Eisenstein-Stern and Stern-Brocot trees via matrix algebra. J. Log. Algebraic Methods Program. 85(5, Part 2), 906–920 (2016). https://doi.org/10.1016/j.jlamp.2015.11.004. http://www.sciencedirect.com/science/article/pii/S2352220815001418. Articles dedicated to Prof. J. N. Oliveira on the occasion of his 60th birthday
Ferreira, J.F., Mendes, A., Backhouse, R., Barbosa, L.S.: Which mathematics for the information society? In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 39–56. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_4
Ferreira, J.F., Mendes, A., Cunha, A., Baquero, C., Silva, P., Barbosa, L.S., Oliveira, J.N.: Logic training through algorithmic problem solving. In: Blackburn, P., van Ditmarsch, H., Manzano, M., Soler-Toscano, F. (eds.) TICTTL 2011. LNCS (LNAI), vol. 6680, pp. 62–69. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21350-2_8
Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Springer, New York (1993)
Gries, D., Schneider, F.B.: Teaching math more effectively, through calculational proofs. Am. Math. Mon. 102(8), 691–697 (1995)
Hinze, R.: Scans and convolutions—a calculational proof of Moessner’s theorem. In: Scholz, S.-B., Chitil, O. (eds.) IFL 2008. LNCS, vol. 5836, pp. 1–24. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24452-0_1
Kahl, W.: Calculational relation-algebraic proofs in Isabelle/Isar. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 178–190. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24771-5_16
Labahn, G., Lank, E., MacLean, S., Marzouk, M., Tausky, D.: Mathbrush: a system for doing math on pen-based devices. In: Proceedings of the 2008 The Eighth IAPR International Workshop on Document Analysis Systems, DAS 2008, pp. 599–606. IEEE Computer Society, Washington, DC (2008). https://doi.org/10.1109/DAS.2008.21
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20
Leino, K.R.M., Polikarpova, N.: Verified calculations. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 170–190. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54108-7_9
Lüth, C., Ring, M.: A web interface for Isabelle: the next generation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 326–329. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_22
Manolios, P., Moore, J.S.: On the desirability of mechanizing calculational proofs. Inf. Process. Lett. 77(2–4), 173–179 (2001). https://doi.org/10.1016/S0020-0190(00)00200-3
Mendes, A.: Structured editing of handwritten mathematics. Ph.D. thesis, School of Computer Science, University of Nottingham (2012)
Mendes, A., Backhouse, R., Ferreira, J.F.: Structure editing of handwritten mathematics: improving the computer support for the calculational method. In: Proceedings of the Ninth ACM International Conference on Interactive Tabletops and Surfaces, ITS 2014, pp. 139–148. ACM, New York (2014). https://doi.org/10.1145/2669485.2669495
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2016). https://doi.org/10.1007/3-540-45949-9. https://isabelle.in.tum.de/doc/prog-prove.pdf
Microsoft OneNote. https://www.onenote.com. Accessed 02 Feb 2018
Pit-Claudel, C., Courtieu, P.: Company-Coq: taking proof general one step closer to a real IDE. In: CoqPL 2016: International Workshop on Coq for Programming Languages (2016)
Tesson, J., Hashimoto, H., Hu, Z., Loulergue, F., Takeichi, M.: Program calculation in Coq. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 163–179. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-17796-5_10
Tripp, S.D., Bichelmeyer, B.: Rapid prototyping: an alternative instructional design strategy. Educ. Tech. Res. Dev. 38(1), 31–44 (1990)
Verhoeven, R., Backhouse, R.: Interfacing program construction and verification. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1128–1146. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48118-4_10. http://dl.acm.org/citation.cfm?id=647545.730778
Wenzel, M.: Isabelle/jEdit – a prover IDE within the PIDE framework. 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. 468–471. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31374-5_38
Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515–530. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08970-6_33
Wenzel, M., Wolff, B.: Isabelle/PIDE as platform for educational tools. arXiv preprint arXiv:1202.4835 (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Mendes, A., Ferreira, J.F. (2018). Towards Verified Handwritten Calculational Proofs. In: Avigad, J., Mahboubi, A. (eds) Interactive Theorem Proving. ITP 2018. Lecture Notes in Computer Science(), vol 10895. Springer, Cham. https://doi.org/10.1007/978-3-319-94821-8_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-94821-8_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94820-1
Online ISBN: 978-3-319-94821-8
eBook Packages: Computer ScienceComputer Science (R0)