Oxford University, UK

Metis 2.0 [Hur03] is a proof tactic used in the HOL4 interactive theorem prover. It works by converting a higher order logic goal to a set of clauses in first order logic, with the property that a refutation of the clause set can be translated to a higher order logic proof of the original goal.

Experiments with various first order calculi
[Hur03] have shown a *given clause
algorithm* and ordered resolution to best suit this application,
and that is what Metis 2.0 implements. Since equality often appears in
higher order logic goals, Metis 2.0 also implements the ordered
paramodulation calculus.

Metis 2.0 is written in Standard ML, for ease of integration with
HOL4. It uses indexes for resolution, paramodulation, (forward)
subsumption and demodulation. It keeps the *Active* clause set
reduced with respect to all the unit equalities so far derived.

In addition to standard size and distance measures, Metis 2.0 uses
finite models to weight clauses in the *Waiting* set. When
integrated with higher order logic, a finite model is manually
constructed to interpret standard functions and relations in such a
way as to make many standard axioms true and negated goals false.
Non-standard functions and relations are interpreted randomly. Since
it is part of the CASC competition rules that standard functions and
relations are obfuscated, Metis 2.0 will back-off to interpreting all
functions and relations randomly (except equality).

Metis 2.0 is free software, released under the GPL. It can be downloaded from

http://www.gilith.com/software/metis

Metis 2.0 uses a fixed strategy for every input problem. Negative literals are always chosen in favour of positive literals, and terms are ordered using the Knuth-Bendix ordering with uniform symbol weight and precedence favouring reduced arity.

Running previous versions of Metis on previous MIX problem sets has scored in the bottom half of the table, so that is the expected performance. Metis 2.0 always keeps proofs, so the performance will be no different in the proof classes.

Testing on previous UEQ problem sets has shown Metis to be weak on equality problems, so I expect Metis 2.0 to perform relatively worse on the equality divisions, particularly UEQ.

- Hur03
- Hurd J. (September 2003),
**First-Order Proof Tactics in Higher-Order Logic Theorem Provers**, Archer M., Di Vito B., Muñoz C.,*Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003)*(Rome, Italy), pp.56-68, NASA Technical Report CP-2003-212448, NASA.