Advertisement

Design of Point-and-Click User Interfaces for Proof Assistants

  • Bohua ZhanEmail author
  • Zhenyan JiEmail author
  • Wenfan Zhou
  • Chaozhu Xiang
  • Jie Hou
  • Wenhui Sun
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)

Abstract

In interactive theorem proving, human users interact with proof assistants to construct and verify formal proofs. The most popular proof assistants today all have user interfaces that are largely text-based. This leads to a steep learning curve for new users of these tools. In this paper, we propose a framework for designing user interfaces for proof assistants based on pointing and clicking. While a main goal of the design is ease of learning for new users, we intend for the design to be suitable for real verification tasks. The design is also extensible, allowing custom proof methods and search functionality to be added in a convenient way. We implement our ideas in a web interface, with backend provided by holpy, a new system for interactive theorem proving implemented in Python. The resulting user interface is tested on theorems in logic, sets, functions, Peano arithmetic, and lists, demonstrating its applicability in a wide range of areas.

Keywords

Proof assistants User interface Tactics 

Notes

Acknowledgements

We would like to thank the referees for their helpful comments. This work is supported by the CAS Pioneer Hundred Talents Program under grant No. Y9RC585036.

References

  1. 1.
    The HOL 4 system. http://hol.sourceforge.net/
  2. 2.
    Abrial, J.-R., Cansell, D.: Click’n prove: interactive proofs within set theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 1–24. Springer, Heidelberg (2003).  https://doi.org/10.1007/10930755_1CrossRefGoogle Scholar
  3. 3.
    Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-49812-6CrossRefGoogle Scholar
  4. 4.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science An EATCS Series. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-662-07964-5CrossRefzbMATHGoogle Scholar
  5. 5.
    Bertot, Y., Kahn, G., Théry, L.: Proof by pointing. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 141–160. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-57887-0_94CrossRefGoogle Scholar
  6. 6.
    Bertot, Y., Théry, L.: A generic approach to building user interfaces for theorem provers. J. Symb. Comput. 25(2), 161–194 (1998)CrossRefGoogle Scholar
  7. 7.
    Breitner, J.: Visual theorem proving with the incredible proof machine. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 123–139. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-43144-4_8CrossRefzbMATHGoogle Scholar
  8. 8.
    The JSON data interchange syntax, December 2017. http://ecma-international.org/publications/files/ECMA-ST/ECMA-404.pdf
  9. 9.
    Fulton, N., Mitsch, S., Quesel, J., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, 1–7 August 2015, Proceedings, pp. 527–538 (2015)Google Scholar
  10. 10.
    Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39634-2_14CrossRefGoogle Scholar
  11. 11.
    Hales, T., et al.: A formal proof of the Kepler conjecture. Forum Math. Pi 5, e2 (2017)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03359-9_4CrossRefGoogle Scholar
  13. 13.
    Klein, G., et al.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2:1–2:70 (2014)Google Scholar
  14. 14.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  15. 15.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45949-9CrossRefzbMATHGoogle Scholar
  16. 16.
    Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-71070-7_15CrossRefGoogle Scholar
  17. 17.
    Wenzel, M.: Isar — a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–183. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48256-3_12CrossRefGoogle Scholar
  18. 18.
    Zhan, B.: holpy: Interactive Theorem Proving in Python. arXiv e-prints arXiv:1905.05970, May 2019

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.State Key Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingChina
  2. 2.Beijing Jiaotong UniversityBeijingChina

Personalised recommendations