Tutorial/Propositional_logic.ml

   1 TAUT
   2  `(~input_a ==> (internal <=> T)) /\
   3   (~input_b ==> (output <=> internal)) /\
   4   (input_a ==> (output <=> F)) /\
   5   (input_b ==> (output <=> F))
   6   ==> (output <=> ~(input_a \/ input_b))`;;
   7
   8 TAUT
   9 `(i1 /\ i2 <=> a) /\
  10  (i1 /\ i3 <=> b) /\
  11  (i2 /\ i3 <=> c) /\
  12  (i1 /\ c <=> d) /\
  13  (m /\ r <=> e) /\
  14  (m /\ w <=> f) /\
  15  (n /\ w <=> g) /\
  16  (p /\ w <=> h) /\
  17  (q /\ w <=> i) /\
  18  (s /\ x <=> j) /\
  19  (t /\ x <=> k) /\
  20  (v /\ x <=> l) /\
  21  (i1 \/ i2 <=> m) /\
  22  (i1 \/ i3 <=> n) /\
  23  (i1 \/ q <=> p) /\
  24  (i2 \/ i3 <=> q) /\
  25  (i3 \/ a <=> r) /\
  26  (a \/ w <=> s) /\
  27  (b \/ w <=> t) /\
  28  (d \/ h <=> u) /\
  29  (c \/ w <=> v) /\
  30  (~e <=> w) /\
  31  (~u <=> x) /\
  32  (i \/ l <=> o1) /\
  33  (g \/ k <=> o2) /\
  34  (f \/ j <=> o3)
  35  ==> (o1 <=> ~i1) /\ (o2 <=> ~i2) /\ (o3 <=> ~i3)`;;