Minisat/sat_script.ml

   1
   2 let AND_IMP = prove
   3   (`!a b c. a /\ b ==> c <=> a ==> b ==> c`,CONV_TAC TAUT);;
   4 let AND_IMP2 = prove
   5   (`!a b c. a /\ b ==> c <=> (a<=>T) ==> b ==> c`,CONV_TAC TAUT);;
   6 let AND_IMP3 = prove
   7   (`!a b c. ~a /\ b ==> c <=> (a<=>F) ==> b ==> c`,CONV_TAC TAUT);;
   8
   9 let NOT_NOT = GEN_ALL (hd (CONJUNCTS (SPEC_ALL NOT_CLAUSES)));;
  10
  11 let AND_INV = prove
  12   (`!a. (~a /\ a) <=> F`,CONV_TAC TAUT);;
  13
  14 let AND_INV_IMP = prove
  15   (`!a. a ==> ~a ==> F`,CONV_TAC TAUT);;
  16
  17 let OR_DUAL = prove
  18   (`(~(a \/ b) ==> F) = (~a ==> ~b ==> F)`,CONV_TAC TAUT);;
  19
  20 let OR_DUAL2 = prove
  21   (`(~(a \/ b) ==> F) = ((a==>F) ==> ~b ==> F)`,CONV_TAC TAUT);;
  22
  23 let OR_DUAL3 = prove
  24   (`(~(~a \/ b) ==> F) = (a ==> ~b ==> F)`,CONV_TAC TAUT);;
  25
  26 let AND_INV2 = prove
  27   (`(~a ==> F) ==> (a==>F) ==> F`,CONV_TAC TAUT)
  28
  29 let NOT_ELIM2 = prove
  30 (`(~a ==> F) <=> a`,CONV_TAC TAUT)
  31
  32 let IMP_F_EQ_F = prove
  33   (`!t. (t ==> F) <=> (t <=> F)`,CONV_TAC TAUT);;