/*
  Tautology Checker, based on HOW TO SOLVE IT IN PROLOG, p. 68.
  (c) P. H. Roosen-Runge, 2000.

% Version 2: April 1991. Reads terms from  stdin instead of a file argument.
%                        formulae cleaned up.
%         2.1:           Sets non-variable, non-logical terms to false 
%                        so that, for example, "2." and "[x]." are invalid.
%	  2.3: June 29, 1992.  non-variable, non-logical terms now cause
%		         an error message.
%         2.3.1: August 24. Operator precedences aligned with 
%                        prolog-lib/operators.pl
%         2.4: May 14, 1998.  show counter-examples
%         2.4SWI : June 4, 2000: modified for SWI.
% ============================================================================

  To run this program, construct a data file containing              
  propositional formulae.                                             
                                                                      
  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.)   
                                                                      
  Each formula must end with a period (full stop).  

  Invoke the tautology program with the command                       
            tautology < data                               
*/



:-op(990, yfx, iff).  % Left-associative (yfx) for consistency with
                      % commutative arithmetic operators.
 
:-op(990,yfx,implies). % for consistency with iff
:-op(980,yfx, or).
:-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
:-op(960,yfx, and).
:-op(950,fy,not).

user_error_handler(_,_,_,_) :-  error('!! Something wrong.').

error(Message) :- nl, write(Message), nl, halt.

activate :- write('Version 2.4SWI, June 4, 2000'), nl,
     ( formulae 
     ;
       error('!! Something wrong.')
     ).

prettyPrint(T) :-
	copy_term(T, PrettyPrint),
        numbervars(PrettyPrint,0, _), 
	write(PrettyPrint).

formulae :- read(T), (T==end_of_file, halt ; theorem(T), formulae).

theorem(T) :- nl, nl, 
	prettyPrint(T), nl,
       (false(T), write('* Not valid.'),
	 nl, write('* Counter-example: '), prettyPrint(T), !
       ;
	write('* Valid.')
       ),
       nl.
 
false('false').
false(not 'true') :-!.
false( P iff Q) :- false( (P implies Q) and (Q implies P)).
false( P implies Q) :- false( not P or Q).
false( P or Q ) :- false(P) , false(Q).
false( P and Q) :- false(P) ; false(Q).
false(P xor Q) :- false(not(P iff Q)).
false( not not P) :- false(P).
false( not(P iff Q)) :- false( not(P implies Q) or not(Q implies P)).
false( not(P implies Q)) :- false( not( not P or Q)).
false( not(P or Q)) :- false( not P and not Q).
false( not(P and Q)) :- false( not P or not Q).
false( not(P xor Q)) :- false(P iff Q).
false(X) :- checkNonLogical(X).
checkNonLogical(X) :- nonvar(X), functor(X, F, _), 
	       \+ member(F, [true, false, not, and, or, xor, implies, iff]),
               error('!! Non-logical constant in formula.').



