Lines Matching refs:clause
10 type clause = mlibClause.clause
29 val clauses : clauseset -> clause list
33 val simplify : clauseset -> clause -> clause
34 val strengthen : clauseset -> clause -> clause option
37 val subsumed : clauseset -> clause -> bool
39 (* Add a clause into the set *)
40 val add : clause -> clauseset -> clauseset
42 (* Derive (unfactored) consequences of a clause *)
43 val deduce : clauseset -> clause -> clause list
46 val factor : clause list -> clauseset -> clause list * clauseset