home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / tautology.prolog < prev    next >
Text File  |  2002-07-29  |  3KB  |  102 lines
  1. /*
  2.   Tautology Checker, based on HOW TO SOLVE IT IN PROLOG, p. 68.
  3.  
  4.   P. H. Roosen-Runge, October 1990.
  5. % Version 2: April 1991. Reads terms from  stdin instead of a file argument.
  6. %                        formulae cleaned up.
  7. %         2.1:           Sets non-variable, non-logical terms to false 
  8. %                        so that, for example, "2." and "[x]." are invalid.
  9. %         2.2: Dec. 7.   Modified for Quintus Prolog 3.1
  10. %      2.3: June 29, 1992.  non-variable, non-logical terms now cause
  11. %                 an error message.
  12. %         2.3.1: August 24. Operator precedences aligned with 
  13. %                        prolog-lib/operators.pl
  14. %         2.4: May 14, 1998.  show counter-examples
  15. %         2.4.1: Sept. 29, 2000. better error check.
  16. % ============================================================================
  17.  
  18.   To run this program, construct a data file containing              
  19.   propositional formulae.                                             
  20.                                                                       
  21.   Formulae should only contain upper-case letters for variables, the atoms
  22.   'true' and 'false', the operators 'not', 'and', 'or', 'xor', 'implies', 
  23.   'iff' and parentheses. (The operators are listed here in order of descending
  24.   precedence.)   
  25.                                                                       
  26.   Each formula must end with a period (full stop).  
  27.  
  28.   Invoke the tautology program with the command                       
  29.             tautology < data                               
  30. */
  31.  
  32.  
  33.  
  34. :-op(990, yfx, iff).  % Left-associative (yfx) for consistency with
  35.                       % commutative arithmetic operators.
  36.  
  37. :-op(990,yfx,implies). % for consistency with iff
  38. :-op(980,yfx, or).
  39. :-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
  40. :-op(960,yfx, and).
  41. :-op(950,fy,not).
  42.  
  43.  
  44. :-ensure_loaded(library(basics)).  
  45.  
  46. user_error_handler(_,_,_,_) :-  error('!! Something wrong.').
  47.  
  48. error(Message) :- nl, write(Message), nl, halt.
  49.  
  50. activate :- write('Version 2.4.1, September 29, 2000'), nl,
  51.      ( formulae 
  52.      ;
  53.        error('!! Something wrong.')
  54.      ).
  55.  
  56. prettyPrint(T) :-
  57.     copy_term(T, PrettyPrint),
  58.         numbervars(PrettyPrint,0, _), 
  59.     write(PrettyPrint).
  60.  
  61. formulae :- read(T), (T==end_of_file, halt ; theorem(T), formulae).
  62.  
  63. theorem(T) :- nl, nl, 
  64.     prettyPrint(T), nl,
  65.        (false(T), write('* Not valid.'),
  66.      nl, write('* Counter-example: '), prettyPrint(T), !
  67.        ;
  68.     write('* Valid.')
  69.        ),
  70.        nl.
  71.  
  72. false('false').
  73. false(not 'true') :-!.
  74. false( P iff Q) :- false( (P implies Q) and (Q implies P)).
  75. false( P implies Q) :- false( not P or Q).
  76. false( P or Q ) :- false(P) , false(Q).
  77. false( P and Q) :- false(P) ; false(Q).
  78. false(P xor Q) :- false(not(P iff Q)).
  79. false( not not P) :- false(P).
  80. false( not(P iff Q)) :- false( not(P implies Q) or not(Q implies P)).
  81. false( not(P implies Q)) :- false( not( not P or Q)).
  82. false( not(P or Q)) :- false( not P and not Q).
  83. false( not(P and Q)) :- false( not P or not Q).
  84. false( not(P xor Q)) :- false(P iff Q).
  85. false(X) :- checkNonLogical(X).
  86. checkNonLogical(X) :- nonvar(X), 
  87.     (
  88.      functor(X, F, 0),  \+ member(F, [true, false])
  89.         ; 
  90.      functor(X, F, 1), \+ member(F, [not])
  91.         ;
  92.      functor(X, F, 2), \+ member(F, [and, or, xor, implies, iff])
  93.         ;
  94.          functor(X, _, A), A > 2
  95.  
  96.     ),
  97.         error('!! Non-logical term in formula.').
  98.  
  99. :- save_program(tautology,activate).
  100.  
  101.  
  102.