What's in a Name?

Metis is pronounced "MET iss".

• In Greek mythology, Metis was a Titaness who was the first wife of Zeus and the mother of Athena. She was the goddess of wisdom and deep thought.
• Metis is the innermost moon of Jupiter, lying within the planetary ring. The blob at the bottom of this web page is an image of Metis taken by the Galileo probe.
• The Métis people of Canada are mixed-blood offspring of European fur traders and Cree, Ojibway or Saulteaux women.

History

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.

Author

Metis is maintained by Joe Leslie-Hurd.

Credits

• Larry Paulson provided many useful bug reports and suggestions for improvement.
• Geoff Sutcliffe tirelessly tested Metis to make it TPTP and TSTP compliant.
• The MLton team, particularly Stephen Weeks, supported Metis by making many improvements to the MLton profiling system.
• Metis has been much improved by feedback from HOL4 users, especially Michael Norrish, Konrad Slind and Mike Gordon.
• Metis 1.x used an SML version of the Omega procedure, implemented by Michael Norrish and ported to MLton by Ken Friis Larsen.
• Some early Metis code and example problems were based on the theorem proving examples of John Harrison.