1(* ========================================================================= *) 2(* A HOL INTERFACE TO THE METIS FIRST-ORDER PROVER. *) 3(* Created by Joe Hurd, October 2001 *) 4(* ========================================================================= *) 5 6signature metisTools = 7sig 8 9(* "Metis" trace levels: 10 0: No output 11 1: The equivalent of Meson dots 12 2: Timing information 13 3: More detailed prover information: slice by slice 14 4: Log of each step in proof translation 15 5: Log of each inference during proof search *) 16 17type 'a stream = 'a mlibStream.stream 18type limit = mlibMeter.limit 19type term = Term.term 20type thm = Thm.thm 21type tactic = Abbrev.tactic 22type Query = folTools.Query 23type Result = folTools.Result 24 25(* Parameters *) 26type Fparm = folTools.parameters 27type Mparm = mlibMetis.parameters 28type parameters = {interface : Fparm, solver : Mparm, limit : limit} 29 30val defaults : parameters 31val update_interface : (Fparm -> Fparm) -> parameters -> parameters 32val update_solver : (Mparm -> Mparm) -> parameters -> parameters 33val update_limit : (limit -> limit) -> parameters -> parameters 34 35(* Prolog solver *) 36val PROLOG_SOLVE : thm list -> Query -> Result stream 37 38(* Metis solver *) 39val GEN_METIS_SOLVE : parameters -> thm list -> Query -> Result stream 40 41(* Tactic interface to the metis prover *) 42val GEN_METIS_TAC : parameters -> thm list -> tactic 43 44(* All the following use this limit *) 45val limit : limit ref 46 47(* Canned parameters for common situations *) 48val FO_METIS_TAC : thm list -> tactic (* First-order *) 49val FOT_METIS_TAC : thm list -> tactic (* + types *) 50val HO_METIS_TAC : thm list -> tactic (* Higher-order *) 51val HOT_METIS_TAC : thm list -> tactic (* + types *) 52val FULL_METIS_TAC : thm list -> tactic (* + combinators & booleans *) 53 54(* Simple user interface to the metis prover *) 55val FO_METIS_PROVE : thm list -> term -> thm (* First-order *) 56val FOT_METIS_PROVE : thm list -> term -> thm (* + types *) 57val HO_METIS_PROVE : thm list -> term -> thm (* Higher-order *) 58val HOT_METIS_PROVE : thm list -> term -> thm (* + types *) 59val FULL_METIS_PROVE : thm list -> term -> thm (* + combinators & booleans *) 60 61(* Uses heuristics to apply one of {FO|FOT}, {HO|HOT} or FULL. *) 62val METIS_TAC : thm list -> tactic 63val METIS_PROVE : thm list -> term -> thm 64 65end 66