changelog download home install notes performance

What's in a Name?

Metis is pronounced "MET iss".


Metis began life in August 2001 as an intended replacement for the MESON_TAC proof tactic in HOL4. The first release of Metis in HOL4 (called METIS_TAC) occurred in July 2002 featuring a robust model elimination calculus. By November 2002 Metis also implemented the ordered paramodulation calculus, and shortly after gained some users in the form of HOL4 users wishing to speed up their theory development.

September 2002 marked the appearance of the Metis standalone program, compiled to native code using the MLton compiler. This version of Metis is used for profiling the code and investigating performance on harder problems from the TPTP archive, and from 2007 has been entered in the annual CASC competition for automatic theorem provers.

As of 2010, the latest release of Metis comprises around 15,000 non-comment lines of SML code.


Metis is maintained by Joe Leslie-Hurd.


Metis the moon of Jupiter