22 Transformations of logical statements (logic8)

Run LPL Code  ,  PDF Document

Problem

A list of rules


Listing 15: The Complete Model implemented in LPL [13]
model logic8 "Transformations of logical statements"; 
  set i := [1..5]; 
      j := [1..10]; 
  parameter a; 
  binary variable 
    x{i}; xx{i}; xxx{i,j}; xxxx{j}; v; w; y; z; zz; 
  real variable 
    p [0..10]; r[0..10]; rr [10..30]; --u; o; q{i}; t{i}; tt{j,i}; 
  alldiff variable 
    d{i} [1..5]; 
  constraint 
  -- T0 rules 
  Rule01  : y nor z; 
  Rule02  : y nand z; 
  Rule03  : and{i} x; 
  Rule04  : or{i} x; 
  Rule05  : xor{i} x; 
  Rule06  : nor{i} x; 
  Rule07  : nand{i} x; 
  Rule08  : y <= z <= p; 
  Rule08a : y <= z <= p <= v; 
  -- T1 rules 
  Rule10  : y->z; 
  Rule11  : z<-y; 
  Rule12  : forall{i} x; 
  Rule13  : exist{i} x; 
  Ruel14  : atleast(-2){i} x; 
  Ruel15  : atmost(-2){i} x; 
  Rule16  : exactly(0){i} x; 
  -- T2 rules: 
  Rule20  : ~(~y); 
  Rule21  : ~(y and z); 
  Rule22  : ~(y or z); 
  Rule23  : ~(y<->z); 
  Rule24  : ~(y xor z); 
  Rule25  : ~(y<z); 
  Rule26  : ~(atleast(3){i} x); 
  Rule26a : ~(atleast(0){i} x);  // 0 means #i 
  Rule27  : ~(atmost(2){i} x); 
  Rule28  : ~(exactly(3){i} x); 
  Rule29  : 0 <> y; 
  Rule29a : 0=y; 
  Rule30  : y = z; 
  Rule31  : y <-> z; 
  Rule32  : y <> z; 
  Rule33  : y xor z; 
  Rule34  : exactly(2){i} x; 
  Rule35  : atmost(2){i} x; 
  Rule33a : atmost(0){i} x; 
  Rule36  : atleast(2){i} x; 
  -- T3 rules 
  Rule40  : z or (v and y); 
  Rule40a : (v and y) or z; 
  Rule41  : y or atleast(0){i} x; 
  Rule41a : atleast(0){i} x or y; 
  solve; 
end