share/logic/rtest_logic.mac

   1 (kill(all), 'done);
   2 'done$
   3
   4 (load("logic.lisp"), 'done);
   5 'done$
   6
   7 logic_simp (a or (b or false or (a or b)));
   8 a or b$
   9
  10 logic_simp (b eq a eq false eq true);
  11 a eq b eq false$
  12
  13 logic_simp ((a xor true) xor b xor true);
  14 a xor b$
  15
  16 characteristic_vector (f(x,y,z), x, y, z);
  17 [f(false,false,false),f(false,false,true),f(false,true,false),
  18  f(false,true,true),f(true,false,false),f(true,false,true),f(true,true,false),
  19  f(true,true,true)]$
  20
  21 characteristic_vector (true);
  22 [true]$
  23
  24 characteristic_vector (a xor b);
  25 [false, true, true, false]$
  26
  27 characteristic_vector (a implies b);
  28 [true, true, false, true]$
  29
  30 characteristic_vector (a implies b, a, b);
  31 [true, true, false, true]$
  32
  33 characteristic_vector (a implies b, b, a);
  34 [true, false, true, true]$
  35
  36 zhegalkin_form (a or b or c);
  37 a and b and c xor a and b xor a and c xor b and c xor a xor b xor c$
  38
  39 zhegalkin_form ((a implies b) or c);
  40 a and b and c xor a and b xor a and c xor a xor true$
  41
  42 block([e, f],
  43   e : ((a or b) xor c) and d, f: zhegalkin_form (e),
  44   [logic_equiv (e, f), is(characteristic_vector(e)=characteristic_vector(f))]);
  45 [true, true]$
  46
  47 logic_equiv (x and y eq x, x implies y);
  48 true$
  49
  50 demorgan(dual_function (x or y));
  51 x and y$
  52
  53 self_dual (a);
  54 true$
  55
  56 self_dual (not a);
  57 true$
  58
  59 self_dual (a eq b);
  60 false$
  61
  62 closed_under_f (x and y);
  63 true$
  64
  65 closed_under_f (x or y);
  66 true$
  67
  68 closed_under_t (x and y);
  69 true$
  70
  71 closed_under_t (x or y);
  72 true$
  73
  74 monotonic (a or b);
  75 true$
  76
  77 monotonic (a and b);
  78 true$
  79
  80 monotonic (a implies b);
  81 false$
  82
  83 characteristic_vector (a or b);
  84 [false, true, true, true]$
  85
  86 characteristic_vector (a and b);
  87 [false, false, false, true]$
  88
  89 characteristic_vector (a implies b);
  90 [true, true, false, true]$
  91
  92 characteristic_vector (a xor b);
  93 [false, true, true, false]$
  94
  95 linear(a or b);
  96 false$
  97
  98 linear(a eq b);
  99 true$
 100
 101 zhegalkin_form (a or b);
 102 (a and b) xor a xor b$
 103
 104 zhegalkin_form (a eq b);
 105 a xor b xor true$
 106
 107 functionally_complete (x and y, x xor y);
 108 false$
 109
 110 functionally_complete (x and y, x xor y, true);
 111 true$
 112
 113 functionally_complete (x and y, x or y, not x);
 114 true$
 115
 116 logic_basis (x and y, x or y);
 117 false$
 118
 119 logic_basis (x and y, x or y, not x);
 120 false$
 121
 122 logic_basis (x and y, not x);
 123 true$
 124
 125 logic_basis (x or y, not x);
 126 true$
 127
 128 logic_basis (x and y, x xor y, true);
 129 true$
 130
 131 block([logic_functions : { not x, x nand y, x nor y,
 132                                     x implies y, x and y, x or y,
 133                                     x eq y, x xor y, true, false }],
 134                                     subset (powerset(logic_functions),
 135                                       lambda ([s], apply ('logic_basis, listify(s)))));
 136 {{false, x eq y, x and y}, {false, x eq y, x or y},
 137 {false, x implies y}, {true, x xor y, x and y},
 138 {true, x xor y, x or y}, {not x, x implies y},
 139 {not x, x and y}, {not x, x or y},
 140 {x eq y, x xor y, x and y}, {x eq y, x xor y, x or y},
 141 {x implies y, x xor y}, {x nand y}, {x nor y}}$
 142
 143 logic_diff (a or b or c, a);
 144 (b and c) xor b xor c xor true$
 145
 146 logic_diff (a and b and c, a);
 147 b and c$
 148
 149 logic_diff (a or (not a), a);
 150 false$
 151
 152 demorgan(boolean_form (a implies b implies c));
 153 ((not b) and a) or c$
 154
 155 logic_equiv (boolean_form (a implies b implies c),
 156   zhegalkin_form (a implies b implies c));
 157 true$
 158
 159 demorgan (boolean_form (a nor b nor c));
 160 (not a) and (not b) and (not c)$
 161
 162 pdnf (x implies y);
 163 (x and y) or ((not x) and y) or ((not x) and (not y))$
 164
 165 pcnf (x implies y);
 166 (not x) or y$
 167
 168 /* Ksimplifier */
 169 logic_simplify(((not a) and (not b) and c) or ((not a) and b and c) or (a and (not b) and c) or (a and b and c) or ((not a) and b and (not c)));
 170 ((not a) and b) or c$
 171
 172 logic_simplify(((not a) and b) or (a and b));
 173 b$
 174
 175 logic_simplify (a or (not a) and b);
 176 a or b$
 177
 178 logic_simplify (a or (not a) and (b < 0));
 179 a or (b < 0)$