The goal of the OpenTheory project is to allow proofs to be shared between the different theorem prover implementations of higher order logic, including HOL4, ProofPower/HOL and HOL Light. It is hoped that the OpenTheory format is adopted by the higher order logic theorem proving community, and that a standard library of formalized mathematics can be built up for higher order logic.
In the spirit of the QED Project, the motivation for this combines the aesthetic pleasure of elegant formalization with the practical use of a mathematical library in verification. In addition, it can be viewed as engineering support for intensive formalized mathematics efforts such as the FlySpeck project.
Project Status
The OpenTheory project has published a file format standard for articles containing statements and proofs of theorems. By design articles are not supposed to be self-contained, and may contain external references to theorems, constants and type operators that must be supplied by the theorem proving system reading the article.
The open source opentheory tool has been released to process articles. It can be used to eliminate redundancy, create summaries of required and provided theorems, and concatenate articles.
Publications
- Joe Hurd. OpenTheory: Package management for higher order logic theories. In Gabriel Dos Reis and Laurent Théry, editors, PLMMS '09: Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems, pages 31–37, Munich, Germany, August 2009. ACM. [PDF] [BiBTeX]
History
The OpenTheory project was initiated in 2004 by Joe Hurd (HOL4) and Rob Arthan (ProofPower). If you would like to contribute then please email joe@gilith.com
