OpenTheory Project

opentheory   •   metis   •   chess

The goal of the OpenTheory project is to allow specifications and proofs to be shared between different theorem prover implementations of higher order logic, including HOL Light, HOL4 and ProofPower. OpenTheory packages are a common format to build a standard library of formalized mathematics and verified software.

Get started with OpenTheory by downloading the opentheory tool.

Milestones

• 2017: The hol Haskell library for reading and pretty-printing OpenTheory packages.
• 2016: First publication of a standard for interpretation files describing symbol renamings.
• 2014: OpenTheory interfaces have been developed for HOL Light, HOL4 and ProofPower.
• 2011: Launch of the Gilith OpenTheory repo to support community development of theory packages.
• 2010: First publication of a standard for theory files describing theory packages.
• 2009: First release of the open source opentheory tool to process theory packages.
• 2007: First publication of a standard for article files containing proofs of theorems.
• 2004: The project was initiated by Joe Leslie-Hurd (HOL4) and Rob Arthan (ProofPower).

Resources

• A higher order logic theory package Γ ⊳ Δ consists of a proof that the theorems in Δ logically derive from the assumptions in Γ (plus some package meta-data). See the example package theory for more details.
• A list of frequently asked questions about OpenTheory.
• The archives of the old OpenTheory users mailing list.

Theorem Prover Interfaces

Here are the current theorem prover implementations that can read (R) and/or write (W) theories in OpenTheory format:

Publications

• CANONICAL CITATION: Joe Hurd. The OpenTheory standard theory library. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, Third International Symposium on NASA Formal Methods (NFM 2011), volume 6617 of Lecture Notes in Computer Science, pages 177–191. Springer, April 2011. [paper] [bibtex] [talk]
• Joe Leslie-Hurd. Maintaining verified software. In Chung-chieh Shan, editor, Haskell '13: Proceedings of the 2013 ACM SIGPLAN symposium on Haskell, pages 71–80. ACM, September 2013. [paper] [bibtex] [talk]
• Ramana Kumar. Challenges in using OpenTheory to transport Harrison's HOL model from HOL Light to HOL4. In Blanchette and Urban, editors, Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), volume 14 of EPiC Series, pages 110–116. EasyChair, June 2013. [paper] [bibtex]
• Ramana Kumar and Joe Hurd. Standalone tactics using OpenTheory. In Lennart Beringer and Amy Felty, editors, Third International Conference on Interactive Theorem Proving (ITP 2012), volume 7406 of Lecture Notes in Computer Science, pages 405–411. Springer, August 2012. [paper] [bibtex]
• Joe Hurd. Composable packages for higher order logic theories. In M. Aderhold, S. Autexier, and H. Mantel, editors, Proceedings of the 6th International Verification Workshop (VERIFY 2010), July 2010. [paper] [bibtex] [talk]
• 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. [paper] [bibtex] [talk]