Lines Matching refs:clause
30 type clause
34 val mk_clause : parameters -> thm -> clause
35 val dest_clause : clause -> bits
36 val literals : clause -> formula list
37 val is_empty : clause -> bool
38 val dest_rewr : clause -> int * thm
39 val is_rewr : clause -> bool
40 val rebrand : parameters -> clause -> clause
43 val largest_lits : clause -> (clause * int, formula) maplet list
44 val largest_eqs : clause -> (clause * int * bool, term) maplet list
45 val largest_tms : clause -> (clause * int * int list, term) maplet list
46 val drop_order : clause -> clause
49 val subsumes : clause -> clause -> bool
56 val add : clause -> rewrs -> rewrs
61 (* Simplifying rules: these preserve the clause id *)
62 val INST : subst -> clause -> clause
63 val FRESH_VARS : clause -> clause
64 val NEQ_VARS : clause -> clause
65 val DEMODULATE : mlibUnits.units -> clause -> clause
66 val QREWRITE : rewrs -> clause -> clause
67 val REWRITE : rewrs -> clause -> clause
69 (* Ordered resolution and paramodulation: these generate new clause ids *)
70 val FACTOR : clause -> clause list
71 val RESOLVE : clause * int -> clause * int -> clause
72 val PARAMODULATE : clause * int * bool -> clause * int * int list -> clause
77 | mlibResolution of clause * clause
78 | Paramodulation of clause * clause
79 | Factor of clause
80 val derivation : clause -> derivation
85 val pp_clause : clause pp