Metis 2.1

J. Hurd
Galois, Inc., USA
joe[@]gilith.com

Architecture

Metis 2.1 [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.1 implements. Since equality often appears in interactive theorem prover goals, Metis 2.1 also implements the ordered paramodulation calculus.

Implementation

Metis 2.1 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.1 uses finite models to weight clauses in the Passive 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, but with a bias towards making negated goals false. Since it is part of the CASC competition rules that standard functions and relations are obfuscated, Metis 2.1 will back off to the biased random interpretation of all functions and relations (except equality), using a finite model with 4 elements.

Metis 2.1 reads problems in TPTP format and outputs detailed proofs in TSTP format, where each proof step is one of 6 simple inference rules. Metis 2.1 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.1 is free software, released under the GPL. It can be downloaded from

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

Strategies

Metis 2.1 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.

Expected Competition Performance

The major change between Metis 2.0, which was entered into CASC 21, and Metis 2.1 is the TSTP proof format. There were only minor changes to the core proof engine, so Metis 2.1 is expected to perform at approximately the same level and end up in the lower half of the table.

References

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.