[opentheory-users] Release of opentheory tool supporting version 6 articles

[Joe Leslie-Hurd]

I'm happy to announce that the latest release of the opentheory tool, which is

opentheory 1.3 (release 20141105)

and is available for download at

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

now supports version 6 of the article file format as described in

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

The tool supports a new --output-version parameter to select the
version of articles that it outputs (the default is version 6), so
it's easy to convert between article versions like so:

opentheory info --article -o foo5.art --output-version 5 foo.art
opentheory info --article -o foo6.art --output-version 6 foo.art

I have also modified my OpenTheory fork of HOL Light to emit version 6
articles, including an implementation of new_specification in terms of
the defineConstList command, and have used it to produce a new version
of the standard theory library.

Here is the inference rule count for base-1.159, the latest publicly
released version which uses version 5 articles:

$ opentheory info --inference --article -o base5.art --output-version
5 base-1.159
Inference rules:
eqMp ..................... 96,008
subst .................... 78,087
appThm ................... 68,967
refl ..................... 28,548
deductAntisym ............ 28,334
betaConv ................. 13,357
absThm ................... 12,953
assume .................... 4,181
axiom ..................... 3,185
defineConst ................. 219
defineTypeOp (legacy) ........ 13
Total ................... 333,852

And here's the count for base-1.165, which uses version 6 articles:

$ opentheory info --inference --article -o base6.art --output-version
6 base-1.165
Inference rules:
subst .............. 71,795
eqMp ............... 60,651
appThm ............. 40,755
proveHyp ........... 17,131
betaConv ........... 16,423
absThm ............. 12,532
trans .............. 12,254
refl ............... 10,665
deductAntisym ....... 7,955
sym ................. 7,669
assume .............. 4,222
axiom ............... 3,165
defineConst ........... 159
defineConstList ........ 60
defineTypeOp ........... 13
Total ............. 265,449

As can be seen, adding a handful of derived rules of inference results
in a saving of both inference rule count and also article file size:

$ gzip base5.art base6.art && gzip -l base5.art.gz base6.art.gz
  compressed uncompressed  ratio uncompressed_name
     1482155      9421490  84.2% base5.art
     1125697      7508364  85.0% base6.art

Please have a play with the new release of the opentheory tool and let
me know if you see any issues. I'm especially interested in checking
that it correctly implements the new principle of definition embodied
by the defineConstList command, and I don't have a collection of
interesting examples to try it on. In particular, following the recipe
in Rob's paper for implementing new_specification means that each use
of defineConstList in the standard theory library defines a single
constant.

Cheers,

Joe