Magic tree

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/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 theory 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:

Theorem ProverR/WMaintainer
HOL LightRWJoe Leslie-Hurd and Ramana Kumar
HOL4RWRamana Kumar
IsabelleRBrian Huffman

Publications