demos/logic3.pC

   1 #include <iostream.h>
   2 #include "logic3.ph"
   3
   4 instantiate datatype Wff;
   5
   6
   7 void simplify(Wff wff)
   8 {
   9    cout << "input = " << wff << '\n';
  10
  11    rewrite (wff) type (Wff) of
  12       And(True,X):     X
  13    |  And(X,True):     X
  14    |  And(False,_):    False
  15    |  And(_,False):    False
  16    |  Or(True,_):      True
  17    |  Or(_,True):      True
  18    |  Or(False,X):     X
  19    |  Or(X,False):     X
  20    |  Not True:        False
  21    |  Not False:       True
  22    |  Not(Not X):      X
  23    |  Not(And(X,Y)):   Or(Not(X),Not(Y))
  24    |  Not(Or(X,Y)):    And(Not(X),Not(Y))
  25    |  And(And(X,Y),Z): And(X,And(Y,Z))
  26    |  Or(Or(X,Y),Z):   Or(X,Or(Y,Z))
  27    |  And(a,b) | a==b:  a
  28    |  Or(a,b)  | a==b:  a
  29    |  And(X as Var a,Var b) | a == b: X
  30    |  Or(X as Var a,Var b) | a == b:  X
  31    |  And(X as Var a,Y as Var b) | a > b: And(Y,X)
  32    |  Or(X as Var a,Y as Var b) | a > b: Or(Y,X)
  33    |  And(X as Var a,And(Y as Var b,Z)) | a > b: And(Y,And(X,Z))
  34    |  Or(X as Var a,Or(Y as Var b,Z)) | a > b: Or(Y,Or(X,Z))
  35    |  And(X as Var a,And(Y as Var b,Z)) | a == b: Or(X,Z)
  36    |  Or(X as Var a,Or(Y as Var b,Z)) | a == b: Or(X,Z)
  37    |  Xor(a,b):     Or(And(a,Not b),And(a,Not b))
  38    |  Equiv(a,b):   Or(And(a,b),And(Not a,Not b))
  39    |  Implies(a,b): Or(Not a, b)
  40    end rewrite;
  41
  42    cout << "output = " << wff << '\n';
  43 }
  44
  45 int main()
  46 {
  47    Wff e = And(True,Or(True,Not(Var(#"x"))));
  48    simplify(e);
  49    return 0;
  50 }