Metis 2.3 [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.3 implements. Since equality often appears in interactive theorem prover goals, Metis 2.3 also implements the ordered paramodulation calculus.
Metis 2.3 uses a fixed strategy for every input problem. Negative literals are always chosen over positive literals, and terms are ordered using the Knuth-Bendix ordering with uniform symbol weight and precedence favouring reduced arity.
Metis 2.3 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 age and size measures, Metis 2.3 uses finite models to weight clauses in the Passive set. When integrated with higher order logic, an interpretation of known functions and relations is manually constructed to make many of their standard properties valid in the finite model. For example, the domain of the model is the set {0,...,7}, and the higher order logic arithmetic functions are interpreted in the model modulo 8. Unknown functions and relations are interpreted randomly, but with a bias towards making supporting theorems valid in the model. The finite model strategy carries over to TPTP problems, by manually interpreting a collection of functions and relations that appear in TPTP axiom files in such a way as to make the axioms valid in the model.
Metis 2.3 reads problems in TPTP format and outputs detailed proofs in TSTP format, where each refutation step is one of 6 simple inference rules. Metis 2.3 implements a complete calculus, so when the set of clauses is saturated it can soundly declare the input problem to be unprovable (and outputs the saturation set).
Metis 2.3 is free software, released under the MIT license. It can be downloaded from
http://www.gilith.com/software/metis
There have been only minor changes to Metis 2.3 since CASC J5, so it is expected to perform at approximately the same level in CASC 23 and end up in the lower third of the table.