HOL4 Metis Library Documentation

Quick Guide to Using the HOL4 Metis Library

   At the top of your proof script, write

     load "metisLib";
     open metisLib;

   Opening the Metis library makes available the automatic provers

       METIS_TAC : thm list -> tactic
     METIS_PROVE : thm list -> term -> thm

   which both take a list of theorems that are used to prove the subgoal.

Examples

   prove (``?x. x``, METIS_TAC []);

   prove (``!x. ~(x = 0) ==> ?!y. x = SUC y``,
          METIS_TAC [numTheory.INV_SUC, arithmeticTheory.num_CASES]);

   METIS_PROVE [prim_recTheory.LESS_SUC_REFL, arithmeticTheory.num_CASES]
   ``(!P. (!n. (!m. m < n ==> P m) ==> P n) ==> !n. P n) ==>
     !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> !n. P n``;

How It Works

   This is how METIS_TAC proves a HOL subgoal:

    1. First some HOL conversions and tactics simplify the subgoal and convert
       it to conjunctive normal form.
    2. The normalized problem is mapped to first-order syntax.
    3. The Metis first-order prover attacks the first-order problem, hopefully
       deriving a refutation.
    4. The first-order refutation is translated to a HOL proof of the original
       subgoal.

   For more details on the interface please refer to the [1]System Description.
   To find out more about the Metis first-order prover (including performance
   information) you can visit its [2]own web page.

Comparison with MESON_TAC

   METIS_TAC is generally slower than MESON_TAC on simple problems, but has
   better coverage. For example, MESON_TAC cannot prove the following theorems:

     METIS_PROVE [] ``?x. x``;
     METIS_PROVE [] ``p (\x. x) /\ q ==> q /\ p (\y. y)``;

   The combination of model elimination and resolution calculi in METIS_TAC
   allows some hard theorems to be proved that are too deep for the HOL version
   of MESON_TAC, such as the GILMORE_9 and STEAM_ROLLER problems. Also, the
   ordered paramodulation used by the resolution component of METIS_TAC allows
   it to prove harder equality problems. An example to illustrate this is the
   following theorem:

     METIS_PROVE []
     ``(!x y. x * y = y * x) /\ (!x y z. x * y * z = x * (y * z)) ==>
      a * b * c * d * e * f = f * e * d * c * b * a``;

Known Bugs

   At the present time all the bugs are unknown.

Credits

   The HOL4 Metis library was written by Joe Hurd, based on John Harrison's
   implementation of MESON_TAC. The library has been much improved by feedback
   from HOL4 users, especially Michael Norrish, Konrad Slind and Mike Gordon.

Change Log

     * Implemented a HOL specific finite model, which knows about numbers,
       lists and sets.
     * Removed multiple provers, METIS_TAC is now solely based on ordered
       resolution.
     * Changed the normalization to eliminate let terms.

  Version 1.5: 14 January 2004

   Subgoals proved by MESON_TAC when HOL is built .......... 2010
   Proved by METIS_TAC within 10s .......................... 1998

  Between Versions 1.4 and 1.5

     * Scheduling provers is no longer based on time used, but rather number of
       inferences.
     * Simplification of resolution clauses using disequation literals.
     * Implemented finite models to guide clause selection in resolution.
     * The model elimination prover optimizes the order of rules and literals
       within rules.

  Version 1.4: 2 October 2003

   Subgoals proved by MESON_TAC when HOL is built .......... 1982
   Proved by METIS_TAC within 10s .......................... 1977

  Between Versions 1.3 and 1.4

     * Added an ordered resolution prover to the default set.
     * Improved resolution performance with a special-purpose datatype for
       inter-reducing equations.

  Version 1.3: 18 June 2003

   Subgoals proved by MESON_TAC when HOL is built .......... 1976
   Proved by METIS_TAC within 10s .......................... 1971

  Between Versions 1.2 and 1.3

     * Implemention of definitional CNF to reduce blow-up in number of clauses
       (usually caused by nested boolean equivalences).
     * Resolution is more robust and efficient, and includes an option (off by
       default) for clauses to inherit ordering constraints.

  Version 1.2: 19 November 2002

   Subgoals proved by MESON_TAC when HOL is built .......... 1779
   Proved by METIS_TAC within 10s .......................... 1774

  Between Versions 1.1 and 1.2

     * Ground-up rewrite of the resolution calculus, which now performs ordered
       resolution and ordered paramodulation.
     * A single entry-point METIS_TAC, which uses heuristics to decide whether
       to apply FO_METIS_TAC or HO_METIS_TAC.
     * {HO|FO}_METIS_TAC  both  initially  operate  in typeless mode, and
       automatically try again with types if an error occurs during proof
       translation.
     * Extensionality theorem now included in HO_METIS_TAC by default.

  Version 1.1: 21 September 2002

   Subgoals proved by MESON_TAC when HOL is built .......... 1745
   Proved by FO_METIS_TAC within 10s ....................... 1485
   Proved by HO_METIS_TAC within 10s ....................... 1698
   Proved by one of {FO|HO}_METIS_TAC within 10s ........... 1717

  Between Versions 1.0 and 1.1

     * Added a "metis" entry to the HOL trace system: it nows prints status
       information during proof (if HOL is in interactive mode).
     * Restricted (universal and existential) quantifiers are now normalized by
       the NNF conversion.
     * Improved performance in the model elimination proof procedure with
       better caching (following a suggestion from John Harrison).
     * First-order substitutions are now fully Boultonized.
     * The  first-order  logical  kernel automatically performs peep-hole
       optimizations to keep proofs as small as possible.

  Version 1.0: 18 July 2002

   Subgoals proved by MESON_TAC when HOL is built .......... 1435
   Proved by FO_METIS_TAC within 10s ....................... 1240
   Proved by HO_METIS_TAC within 10s ....................... 1346
   Proved by one of {FO|HO}_METIS_TAC within 10s ........... 1389

   Metis the moon of Jupiter

References

   1. http://www.cl.cam.ac.uk/~jeh1004/research/papers/hol2fol.html
   2. http://www.cl.cam.ac.uk/~jeh1004/software/metis