prop-src/T11.pcc

   1 datatype Wff :: collectable
   2              = T | F
   3              | VAR Quark
   4              | NOT Wff
   5              | AND Wff, Wff
   6              | OR  Wff, Wff
   7              ;
   8
   9 refine class Wff::Wff() { cerr << "this"; }
  10    and class Wff::VAR() { cerr << "var"; }
  11    and class Wff::NOT() { cerr << "not"; }
  12    and class Wff::AND() { cerr << "and"; }
  13    and class Wff::OR()  { cerr << "or"; }
  14    and class Wff::~Wff() { cerr << "~wff"; }
  15    and class Wff::~VAR() { cerr << "~var"; }
  16    and class Wff::~NOT() { cerr << "~not"; }
  17    and class Wff::~AND() { cerr << "~and"; }
  18    and class Wff::~OR()  { cerr << "~or"; }
  19 ;
  20
  21 instantiate datatype Wff;
  22
  23 Wff dnf (Wff wff)
  24 {
  25    rewrite (wff) type (Wff)
  26    {  NOT T: F
  27    |  NOT F: T
  28    |  NOT NOT X: X
  29    |  OR(T,_): T
  30    |  OR(_,T): T
  31    |  OR(F,X): X
  32    |  OR(X,F): X
  33    |  AND(T,X): X
  34    |  AND(X,T): X
  35    |  AND(F,_): F
  36    |  AND(_,F): F
  37
  38    |  NOT(OR(X,Y)):   AND(NOT X,NOT Y)
  39
  40    |  AND(OR(X,Y),Z): OR(AND(X,Z),AND(Y,Z))
  41    |  AND(X,OR(Y,Z)): OR(AND(X,Y),AND(X,Z))
  42    |  OR(OR(X,Y),Z):  OR(X,OR(Y,Z))
  43    |  AND(AND(X,Y),Z): AND(X,AND(Y,Z))
  44    }
  45    return wff;
  46 }