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