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 >
Text File  |  2000-01-24  |  651b  |  25 lines
  1. % LOGIC MODULE (used by prover, wp.pl, and useful for symbex)
  2.  
  3. not false ->> true.
  4. not true ->> false.
  5. not not X ->> X.
  6. not(not X and not Y) ->> X or Y.
  7. not(not X or not Y) ->> X and Y.
  8. true implies X ->> X.
  9. X implies true ->> true.
  10. false implies X ->> true.
  11. X implies false ->> not X.
  12. X or false ->> X.
  13. X and false ->> false.
  14. X and X ->> X.
  15. true and X ->> X.
  16. X and true ->> X.
  17. X and (true and Y) ->> X and Y.
  18. X and Y and Y ->> X and Y.
  19. not X and X ->> false.
  20. X and Y and not Y ->> X.
  21. (X or Y) and Z ->> X and Z or Y and Z.
  22.  
  23. X or Y implies Y ->> X implies Y.
  24. (X or (P and Q)) implies P ->> X implies P.
  25. (X or (Q and P)) implies P ->> X implies P.