- let or_op (phi : clause_op) (psi : clause_op) =
- negate_op (and_op (negate_op phi) (negate_op psi))
+ let or_op (phi : clause) (psi : clause) =
+ fun one_dpm -> unit_set (
+ fun (r, h) ->
+ in let truth_value' = (
+ truths (phi one_dpm) (r, h) <> [] ||
+ truths (bind_set (negate_op phi one_dpm) psi) (r, h) <> []
+ ) in (truth_value', r, h))
+
+ let if_op (phi : clause) (psi : clause) : clause =
+ fun one_dpm -> unit_set (
+ fun (r, h) ->
+ in let truth_value' = List.for_all (fun one_dpm ->
+ let (truth_value, _, _) = one_dpm (r, h)
+ in truth_value = false || truths (psi one_dpm) (r, h) <> []
+ ) (phi one_dpm)
+ in (truth_value', r, h));;