home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
ftp.cs.yorku.ca 2015
/
ftp.cs.yorku.ca.tar
/
ftp.cs.yorku.ca
/
pub
/
peter
/
SVT
/
logic.simp
< prev
next >
Wrap
Text File
|
2000-01-24
|
651b
|
25 lines
% LOGIC MODULE (used by prover, wp.pl, and useful for symbex)
not false ->> true.
not true ->> false.
not not X ->> X.
not(not X and not Y) ->> X or Y.
not(not X or not Y) ->> X and Y.
true implies X ->> X.
X implies true ->> true.
false implies X ->> true.
X implies false ->> not X.
X or false ->> X.
X and false ->> false.
X and X ->> X.
true and X ->> X.
X and true ->> X.
X and (true and Y) ->> X and Y.
X and Y and Y ->> X and Y.
not X and X ->> false.
X and Y and not Y ->> X.
(X or Y) and Z ->> X and Z or Y and Z.
X or Y implies Y ->> X implies Y.
(X or (P and Q)) implies P ->> X implies P.
(X or (Q and P)) implies P ->> X implies P.