src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Fri Oct 01 15:34:09 2010 +0200 (2010-10-01)
changeset 39901 75d792edf634
parent 39899 608b108ec979
child 39902 bb43fe4fac93
permissions -rw-r--r--
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet@35826
     1
(*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
blanchet@38027
     2
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
blanchet@38027
     3
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@38027
     4
    Author:     Jasmin Blanchette, TU Muenchen
wenzelm@23442
     5
    Copyright   Cambridge University 2007
wenzelm@23447
     6
wenzelm@29266
     7
HOL setup for the Metis prover.
wenzelm@23442
     8
*)
wenzelm@23442
     9
blanchet@35826
    10
signature METIS_TACTICS =
wenzelm@23442
    11
sig
blanchet@39497
    12
  val trace : bool Unsynchronized.ref
blanchet@39497
    13
  val type_lits : bool Config.T
blanchet@39891
    14
  val new_skolemizer : bool Config.T
blanchet@39497
    15
  val metis_tac : Proof.context -> thm list -> int -> tactic
blanchet@39497
    16
  val metisF_tac : Proof.context -> thm list -> int -> tactic
blanchet@39497
    17
  val metisFT_tac : Proof.context -> thm list -> int -> tactic
blanchet@39497
    18
  val setup : theory -> theory
wenzelm@23442
    19
end
wenzelm@23442
    20
blanchet@35826
    21
structure Metis_Tactics : METIS_TACTICS =
wenzelm@23442
    22
struct
wenzelm@23442
    23
blanchet@39494
    24
open Metis_Translate
blanchet@39497
    25
open Metis_Reconstruct
blanchet@35826
    26
blanchet@39899
    27
structure Int_Pair_Graph =
blanchet@39899
    28
  Graph(type key = int * int val ord = prod_ord int_ord int_ord)
blanchet@39899
    29
blanchet@39497
    30
fun trace_msg msg = if !trace then tracing (msg ()) else ()
wenzelm@32955
    31
blanchet@39891
    32
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
blanchet@39891
    33
val (new_skolemizer, new_skolemizer_setup) =
blanchet@39891
    34
  Attrib.config_bool "metis_new_skolemizer" (K false)
wenzelm@23442
    35
blanchet@39497
    36
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
wenzelm@23442
    37
blanchet@39497
    38
fun have_common_thm ths1 ths2 =
blanchet@39497
    39
  exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2)
wenzelm@23442
    40
wenzelm@32956
    41
(*Determining which axiom clauses are actually used*)
blanchet@39419
    42
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
wenzelm@32994
    43
  | used_axioms _ _ = NONE;
paulson@24855
    44
blanchet@39450
    45
val clause_params =
blanchet@39450
    46
  {ordering = Metis_KnuthBendixOrder.default,
blanchet@39450
    47
   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
blanchet@39450
    48
   orderTerms = true}
blanchet@39450
    49
val active_params =
blanchet@39450
    50
  {clause = clause_params,
blanchet@39450
    51
   prefactor = #prefactor Metis_Active.default,
blanchet@39450
    52
   postfactor = #postfactor Metis_Active.default}
blanchet@39450
    53
val waiting_params =
blanchet@39450
    54
  {symbolsWeight = 1.0,
blanchet@39450
    55
   variablesWeight = 0.0,
blanchet@39450
    56
   literalsWeight = 0.0,
blanchet@39450
    57
   models = []}
blanchet@39497
    58
val resolution_params = {active = active_params, waiting = waiting_params}
blanchet@37573
    59
blanchet@39887
    60
(* In principle, it should be sufficient to apply "assume_tac" to unify the
blanchet@39887
    61
   conclusion with one of the premises. However, in practice, this fails
blanchet@39887
    62
   horribly because of the mildly higher-order nature of the unification
blanchet@39887
    63
   problems. Typical constraints are of the form "?x a b =?= b", where "a" and
blanchet@39887
    64
   "b" are goal parameters. *)
blanchet@39897
    65
fun unify_prem_with_concl thy i th =
blanchet@39887
    66
  let
blanchet@39887
    67
    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
blanchet@39897
    68
    val prem = goal |> Logic.strip_assums_hyp |> the_single
blanchet@39897
    69
    val concl = goal |> Logic.strip_assums_concl
blanchet@39887
    70
    fun add_types Tp instT =
blanchet@39887
    71
      if exists (curry (op =) Tp) instT then instT
blanchet@39887
    72
      else Tp :: map (apsnd (typ_subst_atomic [Tp])) instT
blanchet@39887
    73
    fun unify_types (T, U) =
blanchet@39887
    74
      if T = U then
blanchet@39887
    75
        I
blanchet@39887
    76
      else case (T, U) of
blanchet@39887
    77
        (TVar _, _) => add_types (T, U)
blanchet@39887
    78
      | (_, TVar _) => add_types (U, T)
blanchet@39887
    79
      | (Type (s, Ts), Type (t, Us)) =>
blanchet@39887
    80
        if s = t andalso length Ts = length Us then fold unify_types (Ts ~~ Us)
blanchet@39887
    81
        else raise TYPE ("unify_types", [T, U], [])
blanchet@39887
    82
      | _ => raise TYPE ("unify_types", [T, U], [])
blanchet@39887
    83
    fun pair_untyped_aconv (t1, t2) (u1, u2) =
blanchet@39887
    84
      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
blanchet@39887
    85
    fun add_terms tp inst =
blanchet@39887
    86
      if exists (pair_untyped_aconv tp) inst then inst
blanchet@39887
    87
      else tp :: map (apsnd (subst_atomic [tp])) inst
blanchet@39887
    88
    fun is_flex t =
blanchet@39887
    89
      case strip_comb t of
blanchet@39892
    90
        (Var _, args) => forall (is_Bound orf is_Var (*FIXME: orf is_Free*)) args
blanchet@39887
    91
      | _ => false
blanchet@39887
    92
    fun unify_flex flex rigid =
blanchet@39887
    93
      case strip_comb flex of
blanchet@39887
    94
        (Var (z as (_, T)), args) =>
blanchet@39887
    95
        add_terms (Var z,
blanchet@39887
    96
          (* FIXME: reindex bound variables *)
blanchet@39887
    97
          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
blanchet@39887
    98
      | _ => raise TERM ("unify_flex: expected flex", [flex])
blanchet@39887
    99
    fun unify_potential_flex comb atom =
blanchet@39887
   100
      if is_flex comb then unify_flex comb atom
blanchet@39887
   101
      else if is_Var atom then add_terms (atom, comb)
blanchet@39887
   102
      else raise TERM ("unify_terms", [comb, atom])
blanchet@39887
   103
    fun unify_terms (t, u) =
blanchet@39887
   104
      case (t, u) of
blanchet@39887
   105
        (t1 $ t2, u1 $ u2) =>
blanchet@39887
   106
        if is_flex t then unify_flex t u
blanchet@39887
   107
        else if is_flex u then unify_flex u t
blanchet@39887
   108
        else fold unify_terms [(t1, u1), (t2, u2)]
blanchet@39887
   109
      | (_ $ _, _) => unify_potential_flex t u
blanchet@39887
   110
      | (_, _ $ _) => unify_potential_flex u t
blanchet@39887
   111
      | (Var _, _) => add_terms (t, u)
blanchet@39887
   112
      | (_, Var _) => add_terms (u, t)
blanchet@39887
   113
      | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
blanchet@39897
   114
blanchet@39897
   115
    val inst = [] |> unify_terms (prem, concl)
blanchet@39897
   116
    val _ = trace_msg (fn () => cat_lines (map (fn (t, u) =>
blanchet@39897
   117
        Syntax.string_of_term @{context} t ^ " |-> " ^
blanchet@39897
   118
        Syntax.string_of_term @{context} u) inst))
blanchet@39897
   119
    val instT = fold (fn Tp => unify_types (pairself fastype_of Tp)
blanchet@39897
   120
                               handle TERM _ => I) inst []
blanchet@39897
   121
    val inst = inst |> map (pairself (subst_atomic_types instT))
blanchet@39897
   122
    val cinstT = instT |> map (pairself (ctyp_of thy))
blanchet@39897
   123
    val cinst = inst |> map (pairself (cterm_of thy))
blanchet@39897
   124
  in th |> Thm.instantiate (cinstT, []) |> Thm.instantiate ([], cinst) end
blanchet@39897
   125
  handle Empty => th (* ### FIXME *)
blanchet@39887
   126
blanchet@39899
   127
val cluster_ord = prod_ord (prod_ord int_ord int_ord) bool_ord
blanchet@39899
   128
blanchet@39887
   129
(* Attempts to derive the theorem "False" from a theorem of the form
blanchet@39887
   130
   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
blanchet@39887
   131
   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
blanchet@39887
   132
   must be eliminated first. *)
blanchet@39897
   133
fun discharge_skolem_premises ctxt axioms prems_imp_false =
blanchet@39897
   134
  case prop_of prems_imp_false of
blanchet@39897
   135
    @{prop False} => prems_imp_false
blanchet@39897
   136
  | prems_imp_false_prop =>
blanchet@39897
   137
    let
blanchet@39897
   138
      val thy = ProofContext.theory_of ctxt
blanchet@39897
   139
      fun match_term p =
blanchet@39897
   140
        let
blanchet@39897
   141
          val (tyenv, tenv) =
blanchet@39897
   142
            Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
blanchet@39897
   143
          val tsubst =
blanchet@39897
   144
            tenv |> Vartab.dest
blanchet@39899
   145
                 |> sort (cluster_ord
blanchet@39899
   146
                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
blanchet@39897
   147
                                      o fst o fst))
blanchet@39897
   148
                 |> map (Meson.term_pair_of
blanchet@39897
   149
                         #> pairself (Envir.subst_term_types tyenv))
blanchet@39897
   150
        in (tyenv, tsubst) end
blanchet@39897
   151
      fun subst_info_for_prem assm_no prem =
blanchet@39897
   152
        case prem of
blanchet@39897
   153
          _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
blanchet@39897
   154
          let val ax_no = num |> HOLogic.dest_number |> snd in
blanchet@39897
   155
            (ax_no, (assm_no, match_term (nth axioms ax_no |> snd, t)))
blanchet@39897
   156
          end
blanchet@39897
   157
        | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
blanchet@39897
   158
                           [prem])
blanchet@39899
   159
      fun cluster_of_var_name skolem s =
blanchet@39899
   160
        let val (jj, skolem') = Meson_Clausify.cluster_of_zapped_var_name s in
blanchet@39899
   161
          if skolem' = skolem then SOME jj else NONE
blanchet@39899
   162
        end
blanchet@39899
   163
      fun clusters_in_term skolem t =
blanchet@39899
   164
        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
blanchet@39899
   165
      fun deps_for_term_subst (var, t) =
blanchet@39899
   166
        case clusters_in_term false var of
blanchet@39899
   167
          [] => NONE
blanchet@39899
   168
        | [(ax_no, cluster_no)] =>
blanchet@39899
   169
          SOME ((ax_no, cluster_no),
blanchet@39899
   170
                clusters_in_term true t
blanchet@39899
   171
                |> cluster_no > 0 ? cons (ax_no, cluster_no - 1))
blanchet@39899
   172
        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
blanchet@39897
   173
      val prems = Logic.strip_imp_prems prems_imp_false_prop
blanchet@39897
   174
      val substs = map2 subst_info_for_prem (0 upto length prems - 1) prems
blanchet@39899
   175
      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
blanchet@39899
   176
      val clusters = maps (op ::) depss
blanchet@39899
   177
      val ordered_clusters =
blanchet@39899
   178
        Int_Pair_Graph.empty
blanchet@39899
   179
        |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
blanchet@39899
   180
        |> fold Int_Pair_Graph.add_deps_acyclic depss
blanchet@39899
   181
        |> Int_Pair_Graph.topological_order
blanchet@39899
   182
        handle Int_Pair_Graph.CYCLES _ =>
blanchet@39899
   183
               error "Cannot replay Metis proof in Isabelle without axiom of \
blanchet@39899
   184
                     \choice."
blanchet@39901
   185
(* FIXME *)
blanchet@39899
   186
      val _ = tracing ("SUBSTS: " ^ PolyML.makestring substs)
blanchet@39899
   187
      val _ = tracing ("ORDERED: " ^ PolyML.makestring ordered_clusters)
blanchet@39897
   188
    in
blanchet@39887
   189
      Goal.prove ctxt [] [] @{prop False}
blanchet@39897
   190
          (K (cut_rules_tac (map fst axioms) 1
blanchet@39887
   191
              THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
blanchet@39892
   192
              (* two copies are better than one (FIXME) *)
blanchet@39892
   193
              THEN etac @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 1
blanchet@39887
   194
              THEN TRY (REPEAT_ALL_NEW (etac @{thm allE}) 1)
blanchet@39897
   195
              THEN match_tac [prems_imp_false] 1
blanchet@39887
   196
              THEN DETERM_UNTIL_SOLVED
blanchet@39894
   197
                       (rtac @{thm skolem_COMBK_I} 1
blanchet@39897
   198
                        THEN PRIMITIVE (unify_prem_with_concl thy 1)
blanchet@39887
   199
                        THEN assume_tac 1)))
blanchet@39887
   200
    end
blanchet@39887
   201
blanchet@37516
   202
(* Main function to start Metis proof and reconstruction *)
wenzelm@32956
   203
fun FOL_SOLVE mode ctxt cls ths0 =
wenzelm@32956
   204
  let val thy = ProofContext.theory_of ctxt
blanchet@39497
   205
      val type_lits = Config.get ctxt type_lits
blanchet@39901
   206
      val new_skolemizer =
blanchet@39901
   207
        Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt)
blanchet@35826
   208
      val th_cls_pairs =
blanchet@39894
   209
        map2 (fn j => fn th =>
blanchet@39894
   210
                (Thm.get_name_hint th,
blanchet@39901
   211
                 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
blanchet@39894
   212
             (0 upto length ths0 - 1) ths0
blanchet@39887
   213
      val thss = map (snd o snd) th_cls_pairs
blanchet@39887
   214
      val dischargers = map_filter (fst o snd) th_cls_pairs
wenzelm@32956
   215
      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
wenzelm@32956
   216
      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
wenzelm@32956
   217
      val _ = trace_msg (fn () => "THEOREM CLAUSES")
blanchet@39886
   218
      val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
blanchet@39886
   219
      val (mode, {axioms, tfrees, old_skolems}) =
blanchet@39886
   220
        build_logic_map mode ctxt type_lits cls thss
wenzelm@32956
   221
      val _ = if null tfrees then ()
wenzelm@32956
   222
              else (trace_msg (fn () => "TFREE CLAUSES");
blanchet@37643
   223
                    app (fn TyLitFree ((s, _), (s', _)) =>
blanchet@39887
   224
                            trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
wenzelm@32956
   225
      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
wenzelm@32956
   226
      val thms = map #1 axioms
blanchet@39419
   227
      val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
wenzelm@32956
   228
      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
wenzelm@32956
   229
      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
wenzelm@32956
   230
  in
wenzelm@33317
   231
      case filter (is_false o prop_of) cls of
wenzelm@32956
   232
          false_th::_ => [false_th RS @{thm FalseE}]
wenzelm@32956
   233
        | [] =>
blanchet@39497
   234
      case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
blanchet@39497
   235
           |> Metis_Resolution.loop of
blanchet@39419
   236
          Metis_Resolution.Contradiction mth =>
wenzelm@32956
   237
            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
blanchet@39419
   238
                          Metis_Thm.toString mth)
wenzelm@32956
   239
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
wenzelm@32956
   240
                             (*add constraints arising from converting goal to clause form*)
blanchet@39419
   241
                val proof = Metis_Proof.proof mth
blanchet@39886
   242
                val result =
blanchet@39886
   243
                  fold (replay_one_inference ctxt' mode old_skolems) proof axioms
wenzelm@32956
   244
                and used = map_filter (used_axioms axioms) proof
wenzelm@32956
   245
                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
wenzelm@32956
   246
                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
blanchet@39887
   247
                val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
blanchet@39497
   248
                  if have_common_thm used cls then NONE else SOME name)
wenzelm@32956
   249
            in
blanchet@39497
   250
                if not (null cls) andalso not (have_common_thm used cls) then
blanchet@36383
   251
                  warning "Metis: The assumptions are inconsistent."
blanchet@36383
   252
                else
blanchet@36383
   253
                  ();
blanchet@36383
   254
                if not (null unused) then
blanchet@36230
   255
                  warning ("Metis: Unused theorems: " ^ commas_quote unused
blanchet@36230
   256
                           ^ ".")
blanchet@36230
   257
                else
blanchet@36230
   258
                  ();
wenzelm@32956
   259
                case result of
wenzelm@32956
   260
                    (_,ith)::_ =>
blanchet@36230
   261
                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
blanchet@39887
   262
                         [discharge_skolem_premises ctxt dischargers ith])
blanchet@38097
   263
                  | _ => (trace_msg (fn () => "Metis: No result"); [])
wenzelm@32956
   264
            end
blanchet@39419
   265
        | Metis_Resolution.Satisfiable _ =>
wenzelm@32956
   266
            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
blanchet@38097
   267
             [])
wenzelm@32956
   268
  end;
wenzelm@23442
   269
blanchet@38632
   270
(* Extensionalize "th", because that makes sense and that's what Sledgehammer
blanchet@38632
   271
   does, but also keep an unextensionalized version of "th" for backward
blanchet@38632
   272
   compatibility. *)
blanchet@38632
   273
fun also_extensionalize_theorem th =
blanchet@39890
   274
  let val th' = Meson_Clausify.extensionalize_theorem th in
blanchet@38632
   275
    if Thm.eq_thm (th, th') then [th]
blanchet@38632
   276
    else th :: Meson.make_clauses_unsorted [th']
blanchet@38632
   277
  end
blanchet@38632
   278
blanchet@38028
   279
val neg_clausify =
blanchet@38028
   280
  single
blanchet@38028
   281
  #> Meson.make_clauses_unsorted
blanchet@38632
   282
  #> maps also_extensionalize_theorem
blanchet@39890
   283
  #> map Meson_Clausify.introduce_combinators_in_theorem
blanchet@38028
   284
  #> Meson.finish_cnf
blanchet@38028
   285
blanchet@39269
   286
fun preskolem_tac ctxt st0 =
blanchet@39269
   287
  (if exists (Meson.has_too_many_clauses ctxt)
blanchet@39269
   288
             (Logic.prems_of_goal (prop_of st0) 1) then
blanchet@39269
   289
     cnf.cnfx_rewrite_tac ctxt 1
blanchet@39269
   290
   else
blanchet@39269
   291
     all_tac) st0
blanchet@39269
   292
blanchet@38652
   293
val type_has_top_sort =
blanchet@38652
   294
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
blanchet@38652
   295
blanchet@37516
   296
fun generic_metis_tac mode ctxt ths i st0 =
blanchet@37926
   297
  let
blanchet@37926
   298
    val _ = trace_msg (fn () =>
wenzelm@32956
   299
        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
wenzelm@32956
   300
  in
blanchet@37626
   301
    if exists_type type_has_top_sort (prop_of st0) then
blanchet@37516
   302
      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
wenzelm@35568
   303
    else
blanchet@39594
   304
      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
blanchet@39594
   305
                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
blanchet@39594
   306
                  ctxt i st0
wenzelm@32956
   307
  end
wenzelm@23442
   308
blanchet@37516
   309
val metis_tac = generic_metis_tac HO
blanchet@37516
   310
val metisF_tac = generic_metis_tac FO
blanchet@37516
   311
val metisFT_tac = generic_metis_tac FT
wenzelm@23442
   312
blanchet@38632
   313
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
blanchet@38632
   314
   "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
blanchet@38632
   315
   We don't do it for nonschematic facts "X" because this breaks a few proofs
blanchet@38632
   316
   (in the rare and subtle case where a proof relied on extensionality not being
blanchet@38994
   317
   applied) and brings few benefits. *)
blanchet@38632
   318
val has_tvar =
blanchet@38632
   319
  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
blanchet@37516
   320
fun method name mode =
blanchet@37516
   321
  Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
blanchet@38632
   322
    METHOD (fn facts =>
blanchet@38632
   323
               let
blanchet@38632
   324
                 val (schem_facts, nonschem_facts) =
blanchet@38632
   325
                   List.partition has_tvar facts
blanchet@38632
   326
               in
blanchet@38632
   327
                 HEADGOAL (Method.insert_tac nonschem_facts THEN'
blanchet@38632
   328
                           CHANGED_PROP
blanchet@38632
   329
                           o generic_metis_tac mode ctxt (schem_facts @ ths))
blanchet@38632
   330
               end)))
wenzelm@23442
   331
wenzelm@32956
   332
val setup =
blanchet@37516
   333
  type_lits_setup
blanchet@39891
   334
  #> new_skolemizer_setup
blanchet@37516
   335
  #> method @{binding metis} HO "Metis for FOL/HOL problems"
blanchet@37516
   336
  #> method @{binding metisF} FO "Metis for FOL problems"
blanchet@37516
   337
  #> method @{binding metisFT} FT
blanchet@37516
   338
            "Metis for FOL/HOL problems with fully-typed translation"
wenzelm@23442
   339
wenzelm@23442
   340
end;