2026-07-23T04:27:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16711 2024-03-06T10:58:07Z ddc:004 open_access

User Interface Design in the HolPy Theorem Prover (Invited Talk) Zhan, Bohua Proof assistants User interface Proof automation HolPy is a new interactive theorem prover implemented in Python. It is designed to achieve a small trusted-code-base with externally checkable proofs, writing proof automation using a Python API, and permit a wide variety of user interfaces for different application scenarios. In this talk, I will focus on the design of user interfaces in HolPy. While most interactive theorem provers today use text-based user interfaces, there have been several existing work aiming to build point-and-click interfaces where the user perform actions by clicking on part of the goal or choosing from a menu. In our work, we incorporate into the design extensive proof automation and heuristic suggestion mechanisms, allowing construction of proofs on a large scale using this method. We demonstrate the approach in two common scenarios: general-purpose theorem proving and symbolic computation in mathematics. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bohua Zhan 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.2 urn:nbn:de:0030-drops-167117 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.2 eng https://creativecommons.org/licenses/by/4.0/legalcode