Design of Point-and-Click User Interfaces for Proof Assistants
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.
KeywordsProof assistants User interface Tactics
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.
- 1.The HOL 4 system. http://hol.sourceforge.net/
- 8.The JSON data interchange syntax, December 2017. http://ecma-international.org/publications/files/ECMA-ST/ECMA-404.pdf
- 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
- 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
- 18.Zhan, B.: holpy: Interactive Theorem Proving in Python. arXiv e-prints arXiv:1905.05970, May 2019