HolPy：Python中的交互式定理证明
HolPy: Interactive Theorem Proving in Python
摘要：
HolPy是一个用Python实现的交互式定理证明系统。它使用高阶逻辑作为逻辑基础。它的主要功能包括广泛使用宏来生成，检查和存储证明，基于JSON的理论格式，以及用于在Python中实现证明自动化和其他扩展的API。一个点和点击为基础的用户界面，实现了通用的定理证明。我们描述了HolPy的主要设计决策、当前应用和未来计划。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
