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.

Unfortunately there is no documentation for the source code of Metis, but one design goal of the code was to make it readable, and I'd be happy to answer questions about it emailed to metis-users@gilith.com


Is there a Metis mailing list?

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


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.


Metis the moon of Jupiter