Structure mlibMetis
(* ========================================================================= *)
(* THE METIS COMBINATION OF PROOF PROCEDURES FOR FIRST-ORDER LOGIC *)
(* Copyright (c) 2001-2004 Joe Hurd. *)
(* ========================================================================= *)
signature mlibMetis =
sig
(* mlibMetis trace levels:
0: No output
1: Status information during proof search
2: More status information
3: More detailed prover information: slice by slice
4: High-level proof search information
5: Log of every inference during proof search
6: mlibSupport infrastructure such as mlibTermorder *)
type formula = mlibTerm.formula
type thm = mlibThm.thm
type limit = mlibMeter.limit
type solver = mlibSolver.solver
type solver_node = mlibSolver.solver_node
(* Tuning parameters *)
datatype prover =
mlibResolution of mlibResolution.parameters
| mlibMeson of mlibMeson.parameters
| Delta of mlibMeson.parameters
type prover_parameters = prover * mlibSolver.sos_filter option * mlibSolver.cost_fn
type parameters = prover_parameters list
val default_resolution : prover_parameters
val ordered_resolution : prover_parameters
val default_meson : prover_parameters
val default_delta : prover_parameters
val defaults : parameters
val parameters_to_string : parameters -> string
(* The metis combination of solvers *)
val metis' : parameters -> solver_node
val metis : solver_node (* Uses defaults *)
(* A user-friendly interface *)
val settings : parameters ref (* Initially defaults *)
val limit : limit ref (* Initially unlimited *)
val prove : formula -> thm option (* Axiomatizes, then runs metis *)
val query : formula -> solver (* Axiomatizes, then runs prolog *)
end
HOL 4, Kananaskis-14