Examples/prover9.ml

   1 (* ========================================================================= *)
   2 (* Interface to prover9.                                                     *)
   3 (* ========================================================================= *)
   4
   5 (**** NB: this is the "prover9" command invoked by HOL Light.
   6  **** If this doesn't work, set an explicit path to the prover9 binary
   7  ****)
   8
   9 let prover9 = "prover9";;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* Debugging mode (true = keep the Prover9 input and output files)           *)
  13 (* ------------------------------------------------------------------------- *)
  14
  15 let prover9_debugging = ref false;;
  16
  17 (* ------------------------------------------------------------------------- *)
  18 (* Prover9 options. Set to "" for the Prover9 default.                       *)
  19 (* ------------------------------------------------------------------------- *)
  20
  21 let prover9_options = ref
  22 ("clear(auto_inference).\n"^
  23  "clear(auto_denials).\n"^
  24  "clear(auto_limits).\n"^
  25  "set(neg_binary_resolution).\n"^
  26  "set(binary_resolution).\n"^
  27  "set(paramodulation).\n");;
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (* Find the variables, functions, and predicates excluding equality.         *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 let rec functions fvs tm (vacc,facc,racc as acc) =
  34   if is_var tm then
  35     if mem tm fvs then (vacc,insert tm facc,racc)
  36     else (insert tm vacc,facc,racc)
  37   else if is_abs tm then acc else
  38   let f,args = strip_comb tm in
  39   itlist (functions fvs) args (vacc,insert f facc,racc);;
  40
  41 let rec signature fvs tm (vacc,facc,racc as acc) =
  42   if is_neg tm then signature fvs (rand tm) acc
  43   else if is_conj tm or is_disj tm or is_imp tm or is_iff tm then
  44     signature fvs (lhand tm) (signature fvs (rand tm) acc)
  45   else if is_forall tm or is_exists tm or is_uexists tm then
  46     signature fvs (body(rand tm)) acc
  47   else if is_eq tm then
  48     functions fvs (lhand tm) (functions fvs (rand tm) acc)
  49   else if is_abs tm then acc else
  50   let r,args = strip_comb tm in
  51   itlist (functions fvs) args (vacc,facc,insert r racc);;
  52
  53 (* ------------------------------------------------------------------------- *)
  54 (* Shadow first-order syntax. Literal sign is true = positive.               *)
  55 (* ------------------------------------------------------------------------- *)
  56
  57 type folterm = Variable of string | Function of string * folterm list;;
  58
  59 type literal = Literal of bool * string * folterm list;;
  60
  61 (* ------------------------------------------------------------------------- *)
  62 (* Translate clause into shadow syntax.                                      *)
  63 (* ------------------------------------------------------------------------- *)
  64
  65 let rec translate_term (trans_var,trans_fun,trans_rel as trp) tm =
  66   let f,args = strip_comb tm in
  67   if defined trans_fun f then
  68     Function(apply trans_fun f,map (translate_term trp) args)
  69   else if is_var tm then Variable(apply trans_var tm)
  70   else failwith("unknown function"^
  71                 (try fst(dest_const tm) with Failure _ -> "??"));;
  72
  73 let translate_atom (trans_var,trans_fun,trans_rel as trp) tm =
  74   if is_eq tm then
  75     Literal(true,"=",[translate_term trp (lhand tm);
  76                       translate_term trp (rand tm)])
  77   else
  78     let r,args = strip_comb tm in
  79     Literal(true,apply trans_rel r,map (translate_term trp) args);;
  80
  81 let rec translate_clause trp tm =
  82   if is_disj tm then
  83     translate_clause trp (lhand tm) @ translate_clause trp (rand tm)
  84   else if is_neg tm then
  85     let Literal(s,r,args) = translate_atom trp (rand tm) in
  86     [Literal(not s,r,args)]
  87   else [translate_atom trp tm];;
  88
  89 (* ------------------------------------------------------------------------- *)
  90 (* Create Prover9 input file for a set of clauses.                           *)
  91 (* ------------------------------------------------------------------------- *)
  92
  93 let rec prover9_of_term tm =
  94   match tm with
  95     Variable(s) -> s
  96   | Function(f,[]) -> f
  97   | Function(f,args) ->
  98         f^"("^
  99         end_itlist (fun s t -> s^","^t) (map prover9_of_term args) ^
 100         ")";;
 101
 102 let prover9_of_literal lit =
 103   match lit with
 104     Literal(s,r,[]) -> if s then r else "-"^r
 105   | Literal(s,"=",[l;r]) ->
 106         (if s then "(" else "-(")^
 107         (prover9_of_term l) ^ " = " ^ (prover9_of_term r)^")"
 108   | Literal(s,r,args) ->
 109         (if s then "" else "-")^r^"("^
 110         end_itlist (fun s t -> s^","^t) (map prover9_of_term args) ^
 111         ")";;
 112
 113 let rec prover9_of_clause cls =
 114   match cls with
 115     [] -> failwith "prover9_of_clause: empty clause"
 116   | [l] -> prover9_of_literal l
 117   | l::ls -> prover9_of_literal l ^ " | " ^ prover9_of_clause ls;;
 118
 119 (* ------------------------------------------------------------------------- *)
 120 (* Parse S-expressions.                                                      *)
 121 (* ------------------------------------------------------------------------- *)
 122
 123 type sexp = Atom of string | List of sexp list;;
 124
 125 let atom inp =
 126   match inp with
 127     Resword "("::rst -> raise Noparse
 128   | Resword ")"::rst -> raise Noparse
 129   | Resword s::rst -> Atom s,rst
 130   | Ident s::rst -> Atom s,rst
 131   | [] -> raise Noparse;;
 132
 133 let rec sexpression inp =
 134   ( atom
 135  || (a (Resword "(") ++ many sexpression ++ a (Resword ")") >>
 136      (fun ((_,l),_) -> List l)))
 137   inp;;
 138
 139 (* ------------------------------------------------------------------------- *)
 140 (* Skip to beginning of proof object.                                        *)
 141 (* ------------------------------------------------------------------------- *)
 142
 143 let rec skipheader i s =
 144   if String.sub s i 28 = ";; BEGINNING OF PROOF OBJECT"
 145   then String.sub s (i + 28) (String.length s - i - 28)
 146   else skipheader (i + 1) s;;
 147
 148 (* ------------------------------------------------------------------------- *)
 149 (* Parse a proof step.                                                       *)
 150 (* ------------------------------------------------------------------------- *)
 151
 152 let parse_proofstep ps =
 153   match ps with
 154     List[Atom id; just; formula; Atom "NIL"] -> (id,just,formula)
 155   | _ -> failwith "unexpected proofstep";;
 156
 157 (* ------------------------------------------------------------------------- *)
 158 (* Convert sexp representation of formula to shadow syntax.                  *)
 159 (* ------------------------------------------------------------------------- *)
 160
 161 let rec folterm_of_sexp sexp =
 162   match sexp with
 163     Atom(s) when String.sub s 0 1 = "v" -> Variable s
 164   | Atom(s) -> Function(s,[])
 165   | List(Atom f::args) -> Function(f,map folterm_of_sexp args)
 166   | _ -> failwith "folterm_of_sexp: malformed sexpression term representation";;
 167
 168 let folatom_of_sexp sexp =
 169   match sexp with
 170     Atom(r) -> Literal(true,r,[])
 171   | List(Atom r::args) -> Literal(true,r,map folterm_of_sexp args)
 172   | _ -> failwith "folatom_of_sexp: malformed sexpression atom representation";;
 173
 174 let folliteral_of_sexp sexp =
 175   match sexp with
 176     List[Atom "not";sex] -> let Literal(s,r,args) = folatom_of_sexp sex in
 177                              Literal(not s,r,args)
 178   | _ -> folatom_of_sexp sexp;;
 179
 180 let rec folclause_of_sexp sexp =
 181   match sexp with
 182     List[Atom "or";sex1;sex2] ->
 183         folclause_of_sexp sex1 @ folclause_of_sexp sex2
 184   | _ -> [folliteral_of_sexp sexp];;
 185
 186 (* ------------------------------------------------------------------------- *)
 187 (* Convert shadow syntax back into HOL (sometimes given expected type).      *)
 188 (* Make a crude type postcorrection for equations between variables based    *)
 189 (* on their types in other terms, if applicable.                             *)
 190 (* It might be nicer to use preterms to get a systematic use of context, but *)
 191 (* this is a pretty simple problem.                                          *)
 192 (* ------------------------------------------------------------------------- *)
 193
 194 let rec hol_of_folterm (btrans_fun,btrans_rel as trp) ty tm =
 195   match tm with
 196     Variable(x) -> variant (ran btrans_fun) (mk_var(x,ty))
 197   | Function(fs,args) ->
 198         let f = apply btrans_fun fs in
 199         let tys,rty = nsplit dest_fun_ty args (type_of f) in
 200         list_mk_comb(f,map2 (hol_of_folterm trp) tys args);;
 201
 202 let hol_of_folliteral (btrans_fun,btrans_rel as trp) lit =
 203   match lit with
 204     Literal(s,"false",[]) -> if s then mk_const("F",[])
 205                              else mk_neg(mk_const("F",[]))
 206   | Literal(s,"=",[l;r]) ->
 207         let tml_prov = hol_of_folterm trp aty l
 208         and tmr_prov = hol_of_folterm trp aty r in
 209         let ty = if type_of tml_prov <> aty then type_of tml_prov
 210                  else if type_of tmr_prov <> aty then type_of tmr_prov
 211                  else aty in
 212         let ptm = mk_eq(hol_of_folterm trp ty l,hol_of_folterm trp ty r) in
 213         if s then ptm else mk_neg ptm
 214   | Literal(s,rs,args) ->
 215         let r = apply btrans_rel rs in
 216         let tys,rty = nsplit dest_fun_ty args (type_of r) in
 217         let ptm = list_mk_comb(r,map2 (hol_of_folterm trp) tys args) in
 218         if s then ptm else mk_neg ptm;;
 219
 220 let is_truevar (bf,_) tm = is_var tm & not(mem tm (ran bf));;
 221
 222 let rec hol_of_folclause trp cls =
 223   match cls with
 224     [] -> mk_const("F",[])
 225   | [c] -> hol_of_folliteral trp c
 226   | c::cs -> let rawcls = map (hol_of_folliteral trp) cls in
 227              let is_truevar tm = is_var tm &
 228                                  not(mem tm (ran(fst trp))) &
 229                                  not(mem tm (ran(snd trp))) in
 230              let und,dec = partition
 231                (fun t -> is_eq t & is_truevar(lhs t) & is_truevar(rhs t))
 232                rawcls in
 233              if und = [] or dec = [] then list_mk_disj rawcls else
 234              let cxt = map dest_var (filter is_truevar (freesl dec)) in
 235              let correct t =
 236                try let l,r = dest_eq t in
 237                    let ls = fst(dest_var l) and rs = fst(dest_var r) in
 238                    let ty = try assoc ls cxt with Failure _ -> assoc rs cxt in
 239                    mk_eq(mk_var(ls,ty),mk_var(rs,ty))
 240                with Failure _ -> t in
 241              list_mk_disj(map correct rawcls);;
 242
 243 (* ------------------------------------------------------------------------- *)
 244 (* Composed map from sexp to HOL items.                                      *)
 245 (* ------------------------------------------------------------------------- *)
 246
 247 let hol_of_term trp ty sexp = hol_of_folterm trp ty (folterm_of_sexp sexp);;
 248
 249 let hol_of_literal trp sexp = hol_of_folliteral trp (folliteral_of_sexp sexp);;
 250
 251 let hol_of_clause trp sexp = hol_of_folclause trp (folclause_of_sexp sexp);;
 252
 253 (* ------------------------------------------------------------------------- *)
 254 (* Follow paramodulation path                                                *)
 255 (* ------------------------------------------------------------------------- *)
 256
 257 let rec PARA_SUBS_CONV path eth tm =
 258   match path with
 259     [] -> if lhs(concl eth) = tm then eth else failwith "PARA_SUBS_CONV"
 260   | n::rpt -> let f,args = strip_comb tm in
 261               funpow (length args - n) RATOR_CONV (RAND_CONV
 262                 (PARA_SUBS_CONV rpt eth)) tm;;
 263
 264 (* ------------------------------------------------------------------------- *)
 265 (* Pull forward disjunct in clause using prover9/Ivy director string.        *)
 266 (* ------------------------------------------------------------------------- *)
 267
 268 let FRONT1_DISJ_CONV =
 269   GEN_REWRITE_CONV I [TAUT `a \/ b \/ c <=> b \/ a \/ c`] ORELSEC
 270   GEN_REWRITE_CONV I [TAUT `a \/ b <=> b \/ a`];;
 271
 272 let rec FRONT_DISJ_CONV l tm =
 273   match l with
 274     [] | ((Atom "1")::_) -> REFL tm
 275   | (Atom "2")::t -> (RAND_CONV (FRONT_DISJ_CONV t) THENC
 276                       FRONT1_DISJ_CONV) tm
 277   | _ -> failwith "unexpected director string in clause";;
 278
 279 (* ------------------------------------------------------------------------- *)
 280 (* For using paramodulating equation, more convenient to put at the back.    *)
 281 (* ------------------------------------------------------------------------- *)
 282
 283 let AP_IMP =
 284   let pp = MATCH_MP(TAUT `(a ==> b) ==> !x. x \/ a ==> x \/ b`) in
 285   fun t -> SPEC t o pp;;
 286
 287 let rec PARA_BACK_CONV eqdir tm =
 288   match eqdir with
 289     [Atom "1"] when not(is_disj tm) -> REFL tm
 290   | [Atom "2"] when not(is_disj tm) -> SYM_CONV tm
 291   | Atom "2"::eqs -> RAND_CONV (PARA_BACK_CONV eqs) tm
 292   | [Atom "1"; Atom f] when is_disj tm ->
 293         let th1 = if f = "2" then LAND_CONV SYM_CONV tm else REFL tm in
 294         let tm' = rand(concl th1) in
 295         let djs = disjuncts tm' in
 296         let th2 = DISJ_ACI_RULE(mk_eq(tm',list_mk_disj(tl djs @ [hd djs]))) in
 297         TRANS th1 th2
 298   | _ -> failwith "PARA_BACK_CONV";;
 299
 300 (* ------------------------------------------------------------------------- *)
 301 (* Do direct resolution on front clauses.                                    *)
 302 (* ------------------------------------------------------------------------- *)
 303
 304 let RESOLVE =
 305   let resrules = map (MATCH_MP o TAUT)
 306    [`a /\ ~a ==> F`;
 307     `~a /\ a ==> F`;
 308     `a /\ (~a \/ b) ==> b`;
 309     `~a /\ (a \/ b) ==> b`;
 310     `(a \/ b) /\ ~a ==> b`;
 311     `(~a \/ b) /\ a ==> b`;
 312     `(a \/ b) /\ (~a \/ c) ==> b \/ c`;
 313     `(~a \/ b) /\ (a \/ c) ==> b \/ c`] in
 314   fun th1 th2 -> let th = CONJ th1 th2 in tryfind (fun f -> f th) resrules;;
 315
 316 (* ------------------------------------------------------------------------- *)
 317 (* AC rearrangement of disjunction but maybe correcting proforma types in    *)
 318 (* the target term for equations between variables.                          *)
 319 (* ------------------------------------------------------------------------- *)
 320
 321 let ACI_CORRECT th tm =
 322   try EQ_MP (DISJ_ACI_RULE(mk_eq(concl th,tm))) th with Failure _ ->
 323   let cxt = map dest_var (frees(concl th)) in
 324   let rec correct t =
 325     if is_disj t then mk_disj(correct(lhand t),correct(rand t))
 326     else if is_neg t then mk_neg(correct(rand t)) else
 327     (try let l,r = dest_eq t in
 328          let ls = fst(dest_var l) and rs = fst(dest_var r) in
 329          let ty = try assoc ls cxt with Failure _ -> assoc rs cxt in
 330          mk_eq(mk_var(ls,ty),mk_var(rs,ty))
 331      with Failure _ -> t) in
 332   let tm' = correct tm in
 333   EQ_MP (DISJ_ACI_RULE(mk_eq(concl th,tm'))) th;;
 334
 335 (* ------------------------------------------------------------------------- *)
 336 (* Process proof step.                                                       *)
 337 (* ------------------------------------------------------------------------- *)
 338
 339 let rec PROVER9_PATH_CONV l conv =
 340   match l with
 341     Atom "2"::t -> RAND_CONV(PROVER9_PATH_CONV t conv)
 342   | Atom "1"::t -> LAND_CONV(PROVER9_PATH_CONV t conv)
 343   | [] -> conv
 344   | _ -> failwith "PROVER9_PATH_CONV:unknown path";;
 345
 346 let PROVER9_FLIP_CONV tm =
 347   if is_neg tm then RAND_CONV SYM_CONV tm else SYM_CONV tm;;
 348
 349 let process_proofstep ths trp asms (lab,just,fm) =
 350   let tm = hol_of_clause trp fm in
 351   match just with
 352     List[Atom "input"] ->
 353         if is_eq tm & lhs tm = rhs tm then REFL(rand tm) else
 354         tryfind (fun th -> PART_MATCH I th tm) ths
 355   |  List[Atom "flip"; Atom n; List path] ->
 356         let th = apply asms n in
 357         let nth = CONV_RULE(PROVER9_PATH_CONV path PROVER9_FLIP_CONV) th in
 358         if concl nth = tm then nth
 359         else failwith "Inconsistency from flip"
 360   | List[Atom "instantiate"; Atom "0"; List[List[x;Atom".";y]]] ->
 361         let th = REFL(hol_of_term trp aty y) in
 362         if concl th = tm then th
 363         else failwith "Inconsistency from instantiation of reflexivity"
 364   | List[Atom "instantiate"; Atom n; List i] ->
 365         let th = apply asms n
 366         and ilist = map (fun (List[Atom x;Atom"."; y]) -> (y,x)) i in
 367         let xs = map
 368          (fun (y,x) -> find_term (fun v -> is_var v & fst(dest_var v) = x)
 369                                  (concl th)) ilist in
 370         let ys = map2
 371           (fun (y,x) v -> hol_of_term trp (type_of v) y) ilist xs in
 372         INST (zip ys xs) th
 373   | List[Atom "paramod"; Atom eqid; List eqdir; Atom tmid; List dir] ->
 374         let eth = CONV_RULE (PARA_BACK_CONV eqdir) (apply asms eqid)
 375         and tth = apply asms tmid
 376         and path = (map (fun (Atom s) -> int_of_string s) dir) in
 377         let etm = concl eth in
 378         let th =
 379           if is_disj etm then
 380             let djs = disjuncts etm in
 381             let eq = last djs in
 382             let fth = CONV_RULE (PARA_SUBS_CONV path (ASSUME eq)) tth in
 383             MP (itlist AP_IMP (butlast djs) (DISCH eq fth)) eth
 384           else CONV_RULE(PARA_SUBS_CONV path eth) tth in
 385         if concl th = tm then th
 386         else failwith "Inconsistency from paramodulation"
 387   | List[Atom "resolve"; Atom l1; List path1; Atom l2; List path2] ->
 388         let th1 = CONV_RULE (FRONT_DISJ_CONV path1) (apply asms l1)
 389         and th2 = CONV_RULE (FRONT_DISJ_CONV path2) (apply asms l2) in
 390         let th3 = RESOLVE th1 th2 in
 391         ACI_CORRECT th3 tm
 392   | List[Atom "propositional"; Atom l] ->
 393         let th1 = apply asms l in
 394         ACI_CORRECT th1 tm
 395   | _ -> failwith "process_proofstep: no translation";;
 396
 397 let rec process_proofsteps ths trp asms steps =
 398   match steps with
 399     [] -> asms,[]
 400   | ((lab,_,_) as st)::sts ->
 401         (try let th = process_proofstep ths trp asms st in
 402              process_proofsteps ths trp ((lab |-> th) asms) sts
 403          with _ -> asms,steps);;
 404
 405 (* ------------------------------------------------------------------------- *)
 406 (* Main refutation procedure for clauses                                     *)
 407 (* ------------------------------------------------------------------------- *)
 408
 409 let PROVER9_REFUTE ths =
 410   let fvs = itlist (fun th -> union (freesl(hyp th))) ths [] in
 411   let fovars,functions,relations =
 412     signature fvs (end_itlist (curry mk_conj) (map concl ths)) ([],[],[]) in
 413   let trans_var =
 414     itlist2 (fun f n -> f |-> "x"^string_of_int n)
 415             fovars (1--length fovars) undefined
 416   and trans_fun =
 417     itlist2 (fun f n -> f |-> "f"^string_of_int n)
 418             functions (1--length functions) undefined
 419   and trans_rel =
 420     itlist2 (fun f n -> f |-> "R"^string_of_int n)
 421             relations (1--length relations) undefined in
 422   let cls =
 423     map (translate_clause (trans_var,trans_fun,trans_rel) o concl) ths in
 424   let p9cls = map (fun c -> prover9_of_clause c ^".\n") cls in
 425   let p9str = "clear(bell).\n"^ !prover9_options ^
 426               "formulas(sos).\n"^
 427               itlist (^) p9cls
 428               "end_of_list.\n" in
 429   let filename_in = Filename.temp_file "prover9" ".in"
 430   and filename_out = Filename.temp_file "prover9" ".out" in
 431   let _ = file_of_string filename_in p9str in
 432   let retcode = Sys.command
 433    (prover9 ^ " -f " ^ filename_in ^ " | prooftrans ivy >" ^ filename_out) in
 434   if retcode <> 0 then failwith "Prover9 call apparently failed" else
 435   let p9proof = string_of_file filename_out in
 436   let _ = if !prover9_debugging then ()
 437           else (ignore(Sys.remove filename_in);
 438                 ignore(Sys.remove filename_out)) in
 439   let List sexps,unp = sexpression(lex(explode(skipheader 0 p9proof))) in
 440   (if unp <> [Ident ";;"; Ident "END"; Ident "OF";
 441               Ident "PROOF"; Ident "OBJECT"]
 442    then (Format.print_string "Unexpected proof object tail";
 443          Format.print_newline())
 444    else ());
 445   let btrans_fun = itlist (fun (x,y) -> y |-> x) (graph trans_fun) undefined
 446   and btrans_rel = itlist (fun (x,y) -> y |-> x) (graph trans_rel) undefined
 447   and proof = map parse_proofstep sexps in
 448   let asms,undone =
 449     process_proofsteps ths (btrans_fun,btrans_rel) undefined proof in
 450   find (fun th -> concl th = mk_const("F",[])) (map snd (graph asms));;
 451
 452 (* ------------------------------------------------------------------------- *)
 453 (* Hence a prover.                                                           *)
 454 (* ------------------------------------------------------------------------- *)
 455
 456 let PROVER9 =
 457   let prule = MATCH_MP(TAUT `(~p ==> F) ==> p`)
 458   and false_tm = `F` and true_tm = `T` in
 459   let init_conv =
 460     TOP_DEPTH_CONV BETA_CONV THENC
 461     PRESIMP_CONV THENC
 462     CONDS_ELIM_CONV THENC
 463     NNFC_CONV THENC CNF_CONV THENC
 464     DEPTH_BINOP_CONV `(/\)` (SKOLEM_CONV THENC PRENEX_CONV) THENC
 465     GEN_REWRITE_CONV REDEPTH_CONV
 466      [RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM] THENC
 467     GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM DISJ_ASSOC] THENC
 468     GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM CONJ_ASSOC] in
 469   fun tm ->
 470     let tm' = mk_neg tm in
 471     let ith = init_conv tm' in
 472     let itm = rand(concl ith) in
 473     if itm = true_tm then failwith "PROVER9: formula is trivially false" else
 474     if itm = false_tm then prule(fst(EQ_IMP_RULE ith)) else
 475     let evs,bod = strip_exists itm in
 476     let ths = map SPEC_ALL (CONJUNCTS(ASSUME bod)) in
 477     let ths' = end_itlist (@) (map (CONJUNCTS o CONV_RULE CNF_CONV) ths) in
 478     let rth = PROVER9_REFUTE ths' in
 479     let eth = itlist SIMPLE_CHOOSE evs rth in
 480     let sth = PROVE_HYP (UNDISCH(fst(EQ_IMP_RULE ith))) eth in
 481     prule(DISCH tm' sth);;
 482
 483 (* ------------------------------------------------------------------------- *)
 484 (* Examples.                                                                 *)
 485 (* ------------------------------------------------------------------------- *)
 486
 487 let FRIEND_0 = time PROVER9
 488  `(!x:P. ~friend(x,x)) /\ ~(a:P = b) /\ (!x y. friend(x,y) ==> friend(y,x))
 489   ==> (!x. ?y z. friend(x,y) /\ ~friend(x,z)) \/
 490           (!x. ?y z. ~(y = z) /\ ~friend(x,y) /\ ~friend(x,z))`;;
 491
 492 let FRIEND_1 = time PROVER9
 493  `(!x:P. ~friend(x,x)) /\ a IN s /\ b IN s /\ ~(a:P = b) /\
 494   (!x y. friend(x,y) ==> friend(y,x))
 495   ==> (!x. x IN s ==> ?y z. y IN s /\ z IN s /\ friend(x,y) /\ ~friend(x,z)) \/
 496       (!x. x IN s ==> ?y z. y IN s /\ z IN s /\
 497                       ~(y = z) /\ ~friend(x,y) /\ ~friend(x,z))`;;
 498
 499 let LOS = time PROVER9
 500  `(!x y z. P(x,y) /\ P(y,z) ==> P(x,z)) /\
 501   (!x y z. Q(x,y) /\ Q(y,z) ==> Q(x,z)) /\
 502   (!x y. Q(x,y) ==> Q(y,x)) /\
 503   (!x y. P(x,y) \/ Q(x,y)) /\
 504   ~P(a,b) /\ ~Q(c,d)
 505   ==> F`;;
 506
 507 let CONWAY_1 = time PROVER9
 508   `(!x. 0 + x = x) /\
 509    (!x y. x + y = y + x) /\
 510    (!x y z. x + (y + z) = (x + y) + z) /\
 511    (!x. 1 * x = x) /\ (!x. x * 1 = x) /\
 512    (!x y z. x * (y * z) = (x * y) * z) /\
 513    (!x. 0 * x = 0) /\ (!x. x * 0 = 0) /\
 514    (!x y z. x * (y + z) = (x * y) + (x * z)) /\
 515    (!x y z. (x + y) * z = (x * z) + (y * z)) /\
 516    (!x y. star(x * y) = 1 + x * star(y * x) * y) /\
 517    (!x y. star(x + y) = star(star(x) * y) * star(x))
 518    ==> star(star(star(1))) = star(star(1))`;;
 519
 520 let CONWAY_2 = time PROVER9
 521   `(!x. 0 + x = x) /\
 522    (!x y. x + y = y + x) /\
 523    (!x y z. x + (y + z) = (x + y) + z) /\
 524    (!x. 1 * x = x) /\ (!x. x * 1 = x) /\
 525    (!x y z. x * (y * z) = (x * y) * z) /\
 526    (!x. 0 * x = 0) /\ (!x. x * 0 = 0) /\
 527    (!x y z. x * (y + z) = (x * y) + (x * z)) /\
 528    (!x y z. (x + y) * z = (x * z) + (y * z)) /\
 529    (!x y. star(x * y) = 1 + x * star(y * x) * y) /\
 530    (!x y. star(x + y) = star(star(x) * y) * star(x))
 531    ==> !a. star(star(star(star(a)))) = star(star(star(a)))`;;
 532
 533 let ECKMAN_HILTON_1 = time PROVER9
 534  `(!x. 1 * x = x) /\
 535   (!x. x * 1 = x) /\
 536   (!x. 1 + x = x) /\
 537   (!x. x + 1 = x) /\
 538   (!w x y z. (w * x) + (y * z) = (w + y) * (x + z))
 539   ==> !a b. a * b = a + b`;;
 540
 541 let ECKMAN_HILTON_2 = time PROVER9
 542  `(!x. 1 * x = x) /\
 543   (!x. x * 1 = x) /\
 544   (!x. 1 + x = x) /\
 545   (!x. x + 1 = x) /\
 546   (!w x y z. (w * x) + (y * z) = (w + y) * (x + z))
 547   ==> !a b. a * b = b * a`;;
 548
 549 let ECKMAN_HILTON_3 = time PROVER9
 550  `(!x. 1 * x = x) /\
 551   (!x. x * 1 = x) /\
 552   (!x. 0 + x = x) /\
 553   (!x. x + 0 = x) /\
 554   (!w x y z. (w * x) + (y * z) = (w + y) * (x + z))
 555   ==> !a b. a * b = b * a`;;
 556
 557 let ECKMAN_HILTON_4 = time PROVER9
 558  `(!x. 1 * x = x) /\
 559   (!x. x * 1 = x) /\
 560   (!x. 0 + x = x) /\
 561   (!x. x + 0 = x) /\
 562   (!w x y z. (w * x) + (y * z) = (w + y) * (x + z))
 563   ==> !a b. a + b = a * b`;;
 564
 565 let DOUBLE_DISTRIB = time PROVER9
 566  `(!x y z. (x * y) * z = (x * z) * (y * z)) /\
 567   (!x y z. z * (x * y) = (z * x) * (z * y))
 568   ==> !a b c. (a * b) * (c * a) = (a * c) * (b * a)`;;