]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_paramodulation/paramod.mli
update in basic_2
[helm.git] / matita / components / ng_paramodulation / paramod.mli
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
13
14 module type Paramod =
15   sig
16     type t
17     type input
18     type state
19     type szsontology = 
20       | Unsatisfiable of 
21           (t Terms.bag * int * t Terms.substitution * int list) list
22       | GaveUp 
23       | Error of string 
24       | Timeout of int * t Terms.bag
25     type bag = t Terms.bag * int
26     val empty_state : state
27     val bag_of_state :state -> bag
28     val replace_bag : state -> bag -> state
29     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
30     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
31     val forward_infer_step :       
32       state ->
33       t Terms.unit_clause ->
34       int ->
35       state 
36     val goal_narrowing :
37       int 
38       -> int
39       -> float option
40       -> state
41       -> state       
42     val paramod : 
43       useage:bool ->
44       max_steps:int ->
45       ?timeout:float ->
46       bag -> 
47       g_passives:t Terms.unit_clause list -> 
48       passives:t Terms.unit_clause list -> szsontology
49     val demod :
50       state -> input* input -> szsontology
51     val fast_eq_check :
52       state -> input* input -> szsontology
53     val nparamod :
54       useage:bool ->
55       max_steps:int ->
56       ?timeout:float ->
57       state -> 
58       input* input -> 
59       szsontology
60   end
61
62 module Paramod ( B : Orderings.Blob ) : Paramod
63 with type t = B.t and type input = B.input