OpenTheory Project

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

Get started with OpenTheory by downloading the opentheory tool.

Milestones

• 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 summary for more details.
• A list of frequently asked questions about OpenTheory.
• There is a mailing list to discuss OpenTheory, where you can get help using or creating theory packages.

Theorem Prover Interfaces

Here are the current theorem prover implementation interfaces that can read (R) and 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. [PDF] [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. [PDF] [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. [PDF] [BiBTeX]
• 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]