[opentheory-users] Version 6 of the OpenTheory article file format standard
joe at gilith.com
Mon Dec 1 23:32:12 UTC 2014
I'm pleased to announce a new version of the OpenTheory article file
format standard, used for encoding theories of higher order logic. The
new version of the article standard is version 6, and is available at
I would like to thank Rob Arthan, Mario Carneiro, Ramana Kumar and the
others who have contributed to defining version 6 of the article
standard: this is a concrete step towards the goal of sharing theories
between the HOL family of theorem provers.
*** Summary of changes in version 6 of the article file format standard
1. The new command version allows a writer to specify the version of
the OpenTheory article format used in an article so that a reader can
take appropriate action.
2. The new command pragma allows a writer to ask for a reader to take
some implementation-dependent action, e.g., to produce debug output.
3. The new commands proveHyp, sym and trans provide an efficient
implementation of three frequently used derived inference rules
allowing writers to produce more compact article files.
4. The new command defineConstList provides a more abstract principle
for constant definition. This supports recent extensions to HOL4 and
5. The new command hdTl provides a destructor function for lists (an
inverse to the existing cons command). This enables writers to store
constants introduced by the new command defineConstList in the
6. The command defineTypeOp has been changed so that the theorems
giving the defining properties of the abstraction and representation
functions have no free variables.
7. There have been minor clarifications to the description of the
primitive types processed by the virtual machine.
8. A note has been added to clarify the description of the command
The changes between version 5 and version 6 of the article file format
standard are highlighted at
*** Converting between version 5 and version 6 articles
The latest release of the opentheory tool, which is available at
supports a new --output-version parameter to select the version of
articles that it outputs, like so:
opentheory info --article -o output5.art --output-version 5 input.art
opentheory info --article -o output6.art --output-version 6 input.art
In this example the input article input.art can be either version 5 or
The latest release of the OpenTheory standard theory library uses
version 6 articles:
To install the standard theory library using the opentheory tool, type
opentheory install base
and to upgrade an existing installation type
More information about the opentheory-users