home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / OpenProlog / tautology.prolog < prev    next >
Text File  |  1999-04-04  |  2KB  |  80 lines
  1. /*
  2.   Tautology Checker, based on HOW TO SOLVE IT IN PROLOG, p. 68.
  3.  
  4.   copyright P. H. Roosen-Runge, October 1990.
  5.  
  6.   Version 2.5,  April 1999, adapted for Open Prolog.
  7.  
  8.  
  9.    Example:
  10. =====================
  11. formulae. % input to top-level prompt.
  12.  
  13. P or not P.
  14.  
  15.  
  16. A or not A % variables are renamed
  17. * Valid.
  18.  
  19.  
  20.  
  21. P or Q implies P and Q.
  22.  
  23.  
  24. A or B implies A and B
  25. * Not valid.
  26. * Counter-example: true or false implies true and false                                           
  27. ====================                                                                      
  28.   Formulae should only contain upper-case letters for variables, the atoms 'true' and 'false', the operators 'not', 'and', 'or', 'xor', 'implies', 'iff' and parentheses. (The operators are listed here in order of descending precedence.)
  29.    
  30. */
  31.  
  32. :-op(990, yfx, iff).  % left-associative for consistency with
  33.                                % commutative arithmetic operators. 
  34. :-op(990,yfx,implies). % for consistency with iff
  35. :-op(980,yfx, or).
  36. :-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
  37. :-op(960,yfx, and).
  38. :-op(950,fy,not).
  39.  
  40.  
  41. formulae :- read(T), theorem(T), formulae.
  42.  
  43. theorem(T) :-
  44.      nl, nl, prettyPrint(T), nl,
  45.     (
  46.       false(T), write('* Not valid.'), nl, write('* Counter-example: '), prettyPrint(T), !
  47.        ;
  48.         write('* Valid.')
  49.      ),
  50.      nl.
  51.  
  52. % logic rules  
  53. false('false').
  54. false(not 'true') :-!.
  55. false( P iff Q) :- false( (P implies Q) and (Q implies P)).
  56. false( P implies Q) :- false( not P or Q).
  57. false( P or Q ) :- false(P) , false(Q).
  58. false( P and Q) :- false(P) ; false(Q).
  59. false(P xor Q) :- false(not(P iff Q)).
  60. false( not not P) :- false(P).
  61. false( not(P iff Q)) :- false( not(P implies Q) or not(Q implies P)).
  62. false( not(P implies Q)) :- false( not( not P or Q)).
  63. false( not(P or Q)) :- false( not P and not Q).
  64. false( not(P and Q)) :- false( not P or not Q).
  65. false( not(P xor Q)) :- false(P iff Q).
  66. false(X) :- checkNonLogical(X).
  67. checkNonLogical(X) :- 
  68.      nonvar(X), functor(X, F, _), 
  69.         \+ member(F, [true, false, not, and, or, xor, implies, iff]),
  70.      nl,  write('!! Non-logical constant in formula.'), nl.
  71.  
  72. prettyPrint(T) :-
  73.        copy_term(T, PrettyPrint), numbervars(PrettyPrint,0, _), 
  74.        write(PrettyPrint).
  75.  
  76.  
  77.  
  78.  
  79.  
  80.