User Interface Design in the HolPy Theorem Prover (Invited Talk)

Author Bohua Zhan



PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.2.pdf
  • Filesize: 317 kB
  • 1 pages

Document Identifiers

Author Details

Bohua Zhan
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

Cite AsGet BibTex

Bohua Zhan. User Interface Design in the HolPy Theorem Prover (Invited Talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.2

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Proof assistants
  • User interface
  • Proof automation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail