1(* ========================================================================= *)
2(* THE METIS COMBINATION OF PROOF PROCEDURES FOR FIRST-ORDER LOGIC           *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6signature mlibMetis =
7sig
8
9(* mlibMetis trace levels:
10   0: No output
11   1: Status information during proof search
12   2: More status information
13   3: More detailed prover information: slice by slice
14   4: High-level proof search information
15   5: Log of every inference during proof search
16   6: mlibSupport infrastructure such as mlibTermorder *)
17
18type formula     = mlibTerm.formula
19type thm         = mlibThm.thm
20type limit       = mlibMeter.limit
21type solver      = mlibSolver.solver
22type solver_node = mlibSolver.solver_node
23
24(* Tuning parameters *)
25datatype prover =
26  mlibResolution of mlibResolution.parameters
27| mlibMeson of mlibMeson.parameters
28| Delta of mlibMeson.parameters
29type prover_parameters = prover * mlibSolver.sos_filter option * mlibSolver.cost_fn
30type parameters = prover_parameters list
31
32val default_resolution   : prover_parameters
33val ordered_resolution   : prover_parameters
34val default_meson        : prover_parameters
35val default_delta        : prover_parameters
36val defaults             : parameters
37val parameters_to_string : parameters -> string
38
39(* The metis combination of solvers *)
40val metis' : parameters -> solver_node
41val metis  : solver_node                (* Uses defaults *)
42
43(* A user-friendly interface *)
44val settings : parameters ref           (* Initially defaults *)
45val limit    : limit ref                (* Initially unlimited *)
46val prove    : formula -> thm option    (* Axiomatizes, then runs metis *)
47val query    : formula -> solver        (* Axiomatizes, then runs prolog *)
48
49end
50