Frequently Asked Questions About the opentheory Tool

What does the tool do?

The opentheory tool processes OpenTheory packages, which contain statements and proofs of theorems in higher order logic. These packages are used to share proofs between the different theorem prover implementations of higher order logic, including HOL4, ProofPower/HOL and HOL Light. See the OpenTheory project home page for more details.

Where can I download the tool?

The most recent version of the opentheory tool can be downloaded from http://www.gilith.com/software/opentheory/.

Where is the tool documentation?

The doc/notes.html file of the opentheory release contains a collection of links to tool documentation.

Is there an OpenTheory mailing list?

There is an email list for OpenTheory users: you can subscribe and view the archives at http://www.gilith.com/mailman/listinfo/opentheory-users.

What version of ML should I use to compile opentheory?

I strongly recommend using MLton (or Poly/ML) over Moscow ML to run opentheory, for reasons of speed (MLton is about 10 times faster than Moscow ML).

How can I see what theory packages I have installed?

The command

opentheory list

displays all installed packages.

Where are the packages installed?

By default, opentheory installs packages in the directory ~/.opentheory. It is possible to specify a different package directory using the global option -d, --root-dir DIR.

The files for package NAME-VERSION are stored in the subdirectory packages/NAME-VERSION of the package directory.

How can I view the contents of a theory package?

The best way to view the contents of a theory package NAME-VERSION is by opening the file

packages/NAME-VERSION/NAME-VERSION.html

in the package directory.

On the command line, executing

opentheory info --summary NAME-VERSION

prints a text summary of the theory package NAME-VERSION on stdout.

What are the NAME.thy files used for?

The theory file NAME.thy, normally found inside a package directory NAME-VERSION, contains instructions for how to construct the theory exported by the package. This might be as simple as

main {
  article: "NAME.art"
}

which says that the theory is constructed by reading the article file NAME.art, but more complex theories are possible that import and combine other theory packages.

Theory files also contain some meta-information about the package in the form of tags, for example:

name: bool
version: 1.0
description: Basic boolean theory
author: Joe Hurd <joe@gilith.com>
license: MIT

Why do some theory packages contain .art files?

The article: directive in a theory file causes the opentheory tool to read in a file in article format—such files have extension .art.

How can I generate a proof article file from a HOL Light theory file?

  1. First, install the Proof Logging in HOL Light Development Snapshot.
  2. Add the following lines to the top of the HOL Light theory file NAME.ml:

    start_logging ();;
    logfile "THEORY";;

  3. For every theorem THM you'd like to include in the article, add an export_thm command like so:

    let THM = ...HOL Light proof of the theorem... ;;
    export_thm THM;;

  4. Add the following lines to the bottom of the NAME.ml theory file:

    logfile_end ();;
    stop_logging ();;

  5. Run the NAME.ml file through HOL Light in the usual way

    ocaml
    #use "hol.ml";;
    #use "NAME.ml";;

    to generate a raw proof article file and an associated theory file:

    opentheory/articles/THEORY.art
    opentheory/articles/THEORY.thy

  6. The raw proof article file can be compressed and converted to the OpenTheory standard namespace with the command

    opentheory info --article -o THEORY.art opentheory/articles/THEORY.thy

    Running this command will generate the OpenTheory proof article file THEORY.art.

Note: You can change the HOL Light name of the type operators and constants that you define in NAME.ml by adding lines to the opentheory/hol-light.int file.

How can I convert a theory package into a proof article file?

Compile the theory package NAME-VERSION to the proof article file THEORY.art using the command:

opentheory info --article -o THEORY.art NAME-VERSION

How can I read a proof article file into my theorem prover?

Read the proof article file NAME.art into your theorem prover, using existing type operators, constants and theorems for the ones in the input-types, input-consts and assumptions sections of the article summary.

If your higher order logic theorem prover does not already have a reader for proof articles, you can contribute to the OpenTheory project by implementing one yourself! To do this you need to write an ML function that takes as input the article file name, and reads in the commands in the article file one by one, processing them exactly as described in the article file format standard.

It might be useful to refer to the article reader implementation in the opentheory tool (although opentheory needs to keep track of more state to rename and compress articles), in particular the following files in the release:

What is the purpose of the test.sml file in the test directory?

This file is part of the self-test for opentheory. The file is run by Moscow ML, MLton and Poly/ML, generating the files mosml-result, mlton-result and polyml-result (respectively). These are compared to the expected result in the result.ok file.

opentheory