1(* ========================================================================= *)
2(* FIRST-ORDER LOGIC CANONICALIZATION                                        *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6(*
7app load ["mlibUseful", "mlibTerm"];
8*)
9
10structure mlibCanon :> mlibCanon =
11struct
12
13open mlibUseful mlibTerm;
14
15infixr |-> ::>
16
17type subst        = mlibSubst.subst;
18val |<>|          = mlibSubst.|<>|;
19val op ::>        = mlibSubst.::>;
20val term_subst    = mlibSubst.term_subst;
21val formula_subst = mlibSubst.formula_subst;
22
23(* ------------------------------------------------------------------------- *)
24(* Helper functions.                                                         *)
25(* ------------------------------------------------------------------------- *)
26
27fun sym lit =
28  let
29    val (x,y) = dest_eq lit
30    val () = assert (x <> y) (Error "sym: refl")
31  in
32    mk_eq (y,x)
33  end;
34
35(* ------------------------------------------------------------------------- *)
36(* Simplification.                                                           *)
37(* ------------------------------------------------------------------------- *)
38
39fun simplify1 (Not False)           = True
40  | simplify1 (Not True)            = False
41  | simplify1 (Not (Not fm))        = fm
42  | simplify1 (And (False, q))      = False
43  | simplify1 (And (p,     False))  = False
44  | simplify1 (And (True,  q))      = q
45  | simplify1 (And (p,     True))   = p
46  | simplify1 (Or  (False, q))      = q
47  | simplify1 (Or  (p,     False))  = p
48  | simplify1 (Or  (True,  q))      = True
49  | simplify1 (Or  (p,     True))   = True
50  | simplify1 (Imp (False, q))      = True
51  | simplify1 (Imp (True,  q))      = q
52  | simplify1 (Imp (p,     True))   = True
53  | simplify1 (Imp (Not p, False))  = p
54  | simplify1 (Imp (p,     False))  = Not p
55  | simplify1 (Iff (True,  q))      = q
56  | simplify1 (Iff (p,     True))   = p
57  | simplify1 (Iff (False, Not q))  = q
58  | simplify1 (Iff (False, q))      = Not q
59  | simplify1 (Iff (Not p, False))  = p
60  | simplify1 (Iff (p,     False))  = Not p
61  | simplify1 (fm as Forall (x, p)) = if mem x (FV p) then fm else p
62  | simplify1 (fm as Exists (x, p)) = if mem x (FV p) then fm else p
63  | simplify1 fm                    = fm;
64
65fun simplify (Not    p)      = simplify1 (Not (simplify p))
66  | simplify (And    (p, q)) = simplify1 (And (simplify p, simplify q))
67  | simplify (Or     (p, q)) = simplify1 (Or  (simplify p, simplify q))
68  | simplify (Imp    (p, q)) = simplify1 (Imp (simplify p, simplify q))
69  | simplify (Iff    (p, q)) = simplify1 (Iff (simplify p, simplify q))
70  | simplify (Forall (x, p)) = simplify1 (Forall (x, simplify p))
71  | simplify (Exists (x, p)) = simplify1 (Exists (x, simplify p))
72  | simplify fm              = fm;
73
74(* ------------------------------------------------------------------------- *)
75(* Negation normal form.                                                     *)
76(* ------------------------------------------------------------------------- *)
77
78fun nnf (And (p,q))     = And (nnf p, nnf q)
79  | nnf (Or (p,q))      = Or (nnf p, nnf q)
80  | nnf (Imp (p,q))     = Or (nnf' p, nnf q)
81  | nnf (Iff (p,q))     = Or (And (nnf p, nnf q), And (nnf' p, nnf' q))
82  | nnf (Forall (x,p))  = Forall (x, nnf p)
83  | nnf (Exists (x,p))  = Exists (x, nnf p)
84  | nnf (Not x)         = nnf' x
85  | nnf fm              = fm
86and nnf' True           = False
87  | nnf' False          = True
88  | nnf' (And (p,q))    = Or (nnf' p, nnf' q)
89  | nnf' (Or (p,q))     = And (nnf' p, nnf' q)
90  | nnf' (Imp (p,q))    = And (nnf p, nnf' q)
91  | nnf' (Iff (p,q))    = Or (And (nnf p, nnf' q), And (nnf' p, nnf q))
92  | nnf' (Forall (x,p)) = Exists (x, nnf' p)
93  | nnf' (Exists (x,p)) = Forall (x, nnf' p)
94  | nnf' (Not x)        = nnf x
95  | nnf' fm             = Not fm;
96
97(* ------------------------------------------------------------------------- *)
98(* Prenex normal form.                                                       *)
99(* ------------------------------------------------------------------------- *)
100
101fun pullquants fm =
102  (case fm of
103     And (Forall (x,p), Forall (y,q)) => pullquant_2 fm Forall And x y p q
104   | Or (Exists (x,p), Exists (y,q)) => pullquant_2 fm Exists Or x y p q
105   | And (Forall (x,p), q) => pullquant_l fm Forall And x p q
106   | And (p, Forall (x,q)) => pullquant_r fm Forall And x p q
107   | Or (Forall (x,p), q) => pullquant_l fm Forall Or x p q
108   | Or (p, Forall (x,q)) => pullquant_r fm Forall Or x p q
109   | And (Exists (x,p), q) => pullquant_l fm Exists And x p q
110   | And (p, Exists (x,q)) => pullquant_r fm Exists And x p q
111   | Or (Exists (x,p), q) => pullquant_l fm Exists Or x p q
112   | Or (p, Exists (x,q)) => pullquant_r fm Exists Or x p q
113   | _ => fm)
114and pullquant_l fm Q C x p q =
115  let
116    val x' = variant x (FV fm)
117  in
118    Q (x', pullquants (C (formula_subst ((x |-> Var x') ::> |<>|) p, q)))
119  end
120and pullquant_r fm Q C x p q =
121  let
122    val x' = variant x (FV fm)
123  in
124    Q (x', pullquants (C (p, formula_subst ((x |-> Var x') ::> |<>|) q)))
125  end
126and pullquant_2 fm Q C x y p q =
127  let
128    val x' = variant x (FV fm)
129  in
130    Q (x', pullquants(C (formula_subst ((x |-> Var x') ::> |<>|) p,
131                         formula_subst ((x |-> Var x') ::> |<>|) q)))
132  end;
133
134fun prenex (Forall (x,p)) = Forall (x, prenex p)
135  | prenex (Exists (x,p)) = Exists (x, prenex p)
136  | prenex (And (p,q)) = pullquants (And (prenex p, prenex q))
137  | prenex (Or (p,q)) = pullquants (Or (prenex p, prenex q))
138  | prenex fm = fm;
139
140val pnf = prenex o nnf o simplify;
141
142(* ------------------------------------------------------------------------- *)
143(* Skolemization function.                                                   *)
144(* ------------------------------------------------------------------------- *)
145
146fun skolem avoid (Exists (y,p)) =
147  let
148    val xs = subtract (FV p) [y]
149    val f = variant (if null xs then "c_" ^ y else "f_" ^ y) avoid
150  in
151    skolem avoid (formula_subst ((y |-> Fn (f, map Var xs)) ::> |<>|) p)
152  end
153  | skolem avoid (Forall (x,p)) = Forall (x, skolem avoid p)
154  | skolem avoid (And (p,q)) = skolem2 avoid And p q
155  | skolem avoid (Or (p,q)) = skolem2 avoid Or p q
156  | skolem _ fm = fm
157and skolem2 avoid C p q =
158  let
159    val p' = skolem avoid p
160    val q' = skolem (union (function_names p') avoid) q
161  in
162    C (p',q')
163  end;
164
165fun skolemize fm = skolem (function_names fm) fm;
166
167val full_skolemize = specialize o prenex o skolemize o nnf o simplify;
168
169(* ------------------------------------------------------------------------- *)
170(* A tautology filter for clauses.                                           *)
171(* ------------------------------------------------------------------------- *)
172
173fun tautologous lits =
174  let
175    val (pos,neg) = List.partition positive lits
176    val pos = List.mapPartial (total sym) pos @ pos
177    val neg = map negate neg
178  in
179    not (null (intersect pos neg))
180  end;
181
182(* ------------------------------------------------------------------------- *)
183(* Conjunctive Normal Form.                                                  *)
184(* ------------------------------------------------------------------------- *)
185
186local
187  fun distrib s1 s2 = cartwith union s1 s2;
188
189  fun push (Or (p,q))  = distrib (push p) (push q)
190    | push (And (p,q)) = union (push p) (push q)
191    | push fm = [[fm]];
192in
193  fun simpcnf True = []
194    | simpcnf False = [[]]
195    | simpcnf fm = List.filter (non tautologous) (push fm);
196end;
197
198val clausal =
199  List.concat o map (simpcnf o specialize o prenex) o flatten_conj o
200  skolemize o nnf o simplify;
201
202val purecnf = list_mk_conj o map list_mk_disj o simpcnf;
203
204val cnf = list_mk_conj o map list_mk_disj o clausal;
205
206val is_clause = List.all is_literal o strip_disj o snd o strip_forall;
207
208val is_cnf = List.all is_clause o strip_conj;
209
210(* ------------------------------------------------------------------------- *)
211(* Categorizing sets of clauses.                                             *)
212(* ------------------------------------------------------------------------- *)
213
214datatype prop = Propositional | Effectively_propositional | Non_propositional;
215datatype equal = Non_equality | Equality | Pure_equality;
216datatype horn = Trivial | Unit | Both_horn | Horn | Negative_horn | Non_horn;
217type category = {prop : prop, equal : equal, horn : horn};
218
219fun categorize_clauses fms =
220  let
221    val cls = map (strip_disj o snd o strip_forall) fms
222    val fm = list_mk_conj fms
223    val rels = relations fm
224    val funs = functions fm
225
226    val prop =
227      if List.all (fn (_,n) => n = 0) rels then Propositional
228      else if List.all (fn (_,n) => n = 0) funs then Effectively_propositional
229      else Non_propositional
230
231    val eq =
232      if not (mem eq_rel rels) then Non_equality
233      else if rels = [eq_rel] then Pure_equality
234      else Equality
235
236    val horn =
237      if List.exists null cls then Trivial
238      else if List.all (fn cl => length cl = 1) cls then Unit
239      else
240        let
241          val posl = map (length o List.filter positive) cls
242          val negl = map (length o List.filter negative) cls
243          val pos = List.all (fn n => n <= 1) posl
244          val neg = List.all (fn n => n <= 1) negl
245        in
246          case (pos,neg) of (true,true) => Both_horn
247          | (true,false) => Horn
248          | (false,true) => Negative_horn
249          | (false,false) => Non_horn
250        end
251  in
252    {prop = prop, equal = eq, horn = horn}
253  end;
254
255local
256  fun prop Propositional = "propositional"
257    | prop Effectively_propositional = "effectively propositional"
258    | prop Non_propositional = "non-propositional";
259
260  fun eq Non_equality = "non-equality"
261    | eq Equality = "equality"
262    | eq Pure_equality = "pure equality";
263
264  fun horn Trivial = "trivial"
265    | horn Unit = "unit"
266    | horn Both_horn = "horn (and negative horn)"
267    | horn Horn = "horn"
268    | horn Negative_horn = "negative horn"
269    | horn Non_horn = "non-horn";
270in
271  fun category_to_string {prop = p, equal = e, horn = h} =
272    prop p ^ ", " ^ eq e ^ ", " ^ horn h;
273end;
274
275end
276