Frequently Asked Questions About Metis

Where can I download Metis?

The most recent version of Metis can be downloaded from http://www.gilith.com/software/metis/.

Where is the Metis documentation?

The Metis home page contains a collection of links to resources.

The command metis --help is used to display tool help.

Is there a Metis mailing list?

Not any more. Between 2010 and 2017 there was a mailing list for Metis users; you can view the archives at http://www.gilith.com/metis/mailing-list.

What version of ML should I use to compile Metis?

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

Why are there no paramodulation steps in Metis proofs?

Metis is doing a paramodulation step internally, but this is broken down in the CNF refutation into one of six simple inference rules, which are described in doc/logical-kernel.txt and can be found in the Thm module of the source code.

The approach of breaking proofs down into tiny inference rules is done to make it easier to replay the proofs when Metis is being used as a tactic in a higher order logic theorem prover, but it makes the proofs less readable.