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