HolPy: Interactive Theorem Proving in Python
Bohua Zhan
TL;DR
HolPy is an interactive theorem proving system built in Python that leverages higher-order logic, macros, and a JSON-based theory format, featuring a user-friendly interface and extensible proof automation.
Contribution
HolPy introduces a Python-based interactive theorem prover with macro support, a JSON theory format, and a user interface, enabling extensibility and ease of use.
Findings
Implemented in Python with a point-and-click interface
Supports macros for proof production and checking
Uses JSON format for theories
Abstract
HolPy is an interactive theorem proving system implemented in Python. It uses higher-order logic as the logical foundation. Its main features include a pervasive use of macros in producing, checking, and storing proofs, a JSON-based format for theories, and an API for implementing proof automation and other extensions in Python. A point-and-click-based user interface is implemented for general-purpose theorem proving. We describe the main design decisions of HolPy, current applications, and plans for the future.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Parallel Computing and Optimization Techniques · Formal Methods in Verification