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 ------------------------------------------------------------------------------ Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server from Actuate! Instantly Supercharge Your Business Reports and Dashboards with Interactivity, Sharing, Native Excel Exports, App Integration & more Get technology previously reserved for billion-dollar corporations, FREE http://pubads.g.doubleclick.net/gampad/clk?id=157005751&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
