home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / GNU / tautology.pl < prev    next >
Text File  |  2002-11-04  |  3KB  |  93 lines
  1. /*
  2.   Tautology Checker, based on HOW TO SOLVE IT IN PROLOG, p. 68.
  3.   (c) P. H. Roosen-Runge, 2000.
  4.  
  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.3: June 29, 1992.  non-variable, non-logical terms now cause
  10. %                 an error message.
  11. %         2.3.1: August 24. Operator precedences aligned with 
  12. %                        prolog-lib/operators.pl
  13. %         2.4: May 14, 1998.  show counter-examples
  14. %         2.4GNU: November 4, 2002: modified for GNU Prolog.
  15. % ============================================================================
  16.  
  17.   To run this program, construct a data file containing              
  18.   propositional formulae.                                             
  19.                                                                       
  20.   Formulae should only contain upper-case letters for variables, the atoms
  21.   'true' and 'false', the operators 'not', 'and', 'or', 'xor', 'implies', 
  22.   'iff' and parentheses. (The operators are listed here in order of descending
  23.   precedence.)   
  24.                                                                       
  25.   Each formula must end with a period (full stop).  
  26.  
  27.   Invoke the tautology program with the command                       
  28.             tautology < data                               
  29. */
  30.  
  31.  
  32.  
  33. :-op(990, yfx, iff).  % Left-associative (yfx) for consistency with
  34.                       % commutative arithmetic operators.
  35.  
  36. :-op(990,yfx,implies). % for consistency with iff
  37. :-op(980,yfx, or).
  38. :-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
  39. :-op(960,yfx, and).
  40. :-op(950,fy,not).
  41.  
  42. :- initialization(activate).   % gprolog
  43.  
  44. user_error_handler(_,_,_,_) :-  error('!! Something wrong.').
  45.  
  46. error(Message) :- nl, write(Message), nl, halt.
  47.  
  48. activate :- 
  49.      set_linedit_prompt('|:'), %gprolog
  50.      write('Version 2.4GNU: November 4, 2002'), 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 :- nl, 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), functor(X, F, _), 
  87.            \+ member(F, [true, false, not, and, or, xor, implies, iff]),
  88.                error('!! Non-logical constant in formula.').
  89.  
  90. % :- save_program(tautology,activate).
  91.  
  92.  
  93.