Frequently Asked Questions About the opentheory Tool

What does the tool do?

The opentheory tool processes OpenTheory packages, which contains 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.

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.

How can I view the contents of a theory package?

The command

opentheory compile --summary-text - ~/.opentheory/packages/NAME-VERSION/NAME.thy
compiles a text summary of the theory package NAME-VERSION, and displays it 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

theory { 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: PublicDomain

Why do some theory packages contain .art files?

The article command in a theory file instructs the opentheory tool to read in an article file, which is conventionally saved in a file with .art suffix.

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

First, prepare HOL Light for logging primitive inferences:

  1. Add the logging.ml file to the HOL Light directory.
  2. Make one change to the hol.ml file.

Once HOL Light has been prepared, the theory file NAME.ml can be converted to the proof article file NAME.art by the following steps:

  1. Add the following lines to the top of the NAME.ml theory file:
    start_logging ();;
    logfile "foo";;
  2. Add the following lines to the bottom of the NAME.ml theory file:
    logfile_end ();;
    stop_logging ();;
  3. Running the NAME.ml file through HOL Light in the usual way
    ocaml
    #use "hol.ml";;
    #use "NAME.ml";;
    will generate a raw proof article file called foo.art.
  4. The proof article file foo.art can be compressed and converted to the OpenTheory standard namespace with the command
    opentheory compile --article NAME.art foo.thy
    Running this command will generate the proof article file NAME.art.

How can I import a theory package into my theorem prover?

There are two steps to this:

  1. Compile the theory package to a proof article file using the command
    opentheory compile --article NAME.art ~/.opentheory/packages/NAME-VERSION/NAME.thy
  2. 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 assumed sections of the theory summary.

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

If your higher order logic theorem prover does not already have a reader for proof articles, there are detailed instructions for implementing one in the 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

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, to check that all has gone well.

opentheory