Skip to main content
SpringerLink
Log in

Towards Verified Handwritten Calculational Proofs

(Short Paper)

  • Conference paper
  • First Online:
Book cover Interactive Theorem Proving (ITP 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10895))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. 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)

    Google Scholar 

  2. 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

    Chapter  MATH  Google Scholar 

  3. Backhouse, R.: The calculational method. Inf. Process. Lett. 53(3), 121 (1995)

    Article  Google Scholar 

  4. 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

    Article  MathSciNet  MATH  Google Scholar 

  5. 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

    Chapter  Google Scholar 

  6. 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)

    Google Scholar 

  7. 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

    Chapter  Google Scholar 

  8. 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

    Book  Google Scholar 

  9. 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

    Book  MATH  Google Scholar 

  10. Ferreira, J.F., Mendes, A.: Students’ feedback on teaching mathematics through the calculational method. In: 39th ASEE/IEEE Frontiers in Education Conference. IEEE (2009)

    Google Scholar 

  11. 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

    Article  MathSciNet  MATH  Google Scholar 

  12. 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

    Chapter  Google Scholar 

  13. 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

    Chapter  Google Scholar 

  14. Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Springer, New York (1993)

    Book  Google Scholar 

  15. Gries, D., Schneider, F.B.: Teaching math more effectively, through calculational proofs. Am. Math. Mon. 102(8), 691–697 (1995)

    Article  MathSciNet  Google Scholar 

  16. 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

    Chapter  Google Scholar 

  17. 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

    Chapter  MATH  Google Scholar 

  18. 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

  19. 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

    Chapter  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  21. 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

    Chapter  Google Scholar 

  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

    Article  MathSciNet  MATH  Google Scholar 

  23. Mendes, A.: Structured editing of handwritten mathematics. Ph.D. thesis, School of Computer Science, University of Nottingham (2012)

    Google Scholar 

  24. 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

  25. 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

    Book  MATH  Google Scholar 

  26. Microsoft OneNote. https://www.onenote.com. Accessed 02 Feb 2018

  27. 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)

    Google Scholar 

  28. 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

    Chapter  Google Scholar 

  29. Tripp, S.D., Bichelmeyer, B.: Rapid prototyping: an alternative instructional design strategy. Educ. Tech. Res. Dev. 38(1), 31–44 (1990)

    Article  Google Scholar 

  30. 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

    Chapter  Google Scholar 

  31. 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

    Chapter  Google Scholar 

  32. 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

    Chapter  Google Scholar 

  33. Wenzel, M., Wolff, B.: Isabelle/PIDE as platform for educational tools. arXiv preprint arXiv:1202.4835 (2012)

Download references

Author information

Authors and Affiliations

  1. School of Computing, Teesside University, Middlesbrough, UK

    Alexandra Mendes & João F. Ferreira

  2. HASLab/INESC TEC, Universidade do Minho, Braga, Portugal

    Alexandra Mendes

  3. INESC-ID/IST, University of Lisbon, Lisbon, Portugal

    João F. Ferreira

Authors
  1. Alexandra Mendes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. João F. Ferreira
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexandra Mendes .

Editor information

Editors and Affiliations

  1. Carnegie Mellon University, Pittsburgh, PA, USA

    Jeremy Avigad

  2. Inria, Nantes, France

    Assia Mahboubi

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation