[opentheory-users] Version 6 of the OpenTheory article file format standard

[Joe Leslie-Hurd]

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

http://www.gilith.com/research/opentheory/article-6.html

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.

Cheers,

Joe

*** 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
ProofPower.

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
dictionary.

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
deductAntisym.

The changes between version 5 and version 6 of the article file format
standard are highlighted at

http://www.gilith.com/research/opentheory/article-5-6.html

*** Converting between version 5 and version 6 articles

The latest release of the opentheory tool, which is available at

http://www.gilith.com/software/opentheory/

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
version 6.

The latest release of the OpenTheory standard theory library uses
version 6 articles:

http://opentheory.gilith.com/?pkg=base

To install the standard theory library using the opentheory tool, type

opentheory install base

and to upgrade an existing installation type

opentheory update
opentheory upgrade