English

HolPy: Interactive Theorem Proving in Python

Logic in Computer Science 2020-01-28 v2

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.

Keywords

Cite

@article{arxiv.1905.05970,
  title  = {HolPy: Interactive Theorem Proving in Python},
  author = {Bohua Zhan},
  journal= {arXiv preprint arXiv:1905.05970},
  year   = {2020}
}

Comments

8 pages