%% taut.pl
%% author: Robert Keller
%% tautology checker in Prolog
%%
%% This program checks an expression in the following grammar for
%% being a tautology, satisfiable but not a tautology, or unsatisfiable.
%%
%% To check one expression, simply use analyze(Expression).  
%% For an interactive loop, use 
%%    taut.
%% To check whether an expression is a tautology, use 
%%    tautology(Expression).
%% To check whether an expression is satisfiable, use 
%%    satsifiable(Expression).
%% If the expression is satisfiable, variables will be bound to values that
%% satisfy it.  For example:
%% | ?- satisfy(A>B).
%%
%% A = B = 0 ;
%% 
%% A = 0,
%% B = 1 ;
%% 
%% A = B = 1 ;
%% 
%% no
%%
%% The grammar is:
%%   E -> 0  |  1  |  V  |  !E  |  E+E  |  E*E  |  E>E  |  E=E
%%
%% The order of precedence is: ! * + = >

:- op(350, fx, !).                    %% Define syntax for ! as 'not' operator.
                                      %% This is the only operator not already
                                      %% in Prolog.  (! has the special meaning
                                      %% of "cut" when not used as an operator)

analyze(Expression) :-                %% analyze expression, show result
  analyze(Expression, Result),
  write(Result),
  nl.

analyze(Expression, Result) :-        %% Analyze expression, get result:
  tautology(Expression)               %% Is it a tautology?
  -> Result = 'tautology'
  ;  ( satisfy(Expression)            %% If not, is it satisfiable?
     -> Result = 'satisfiable, not a tautology'
     ;  Result = 'unsatisfiable'
     ).

tautology(Expression) :-              %% An expression is a tautology iff its 
  \+ satisfy(!Expression).            %% negation is not satisfiable.

satisfy(Expression) :-                %% An expression is satisfiable iff
  eval(Expression, Result),           %% some combination evaluates to 1.
  Result == 1.

eval(V, V) :-                         %% Handle variable expressions.
  var(V),
  !,
  possible_value(V).                  %% enumerate possibilities

eval(V, V) :-                         %% Handle constant expressions.
  possible_value(V),
  !.

eval(!Expr, Result) :-                %% Handle negation of an expression.
  !,
  eval(Expr, V),
  (V == 0 -> Result = 1; Result = 0).

eval(Expr, Result) :-                 %% Handle binary operators (+, *, >, =).
  Expr =.. [Op, A, B],
  validOp(Op),                        %% Check operator validity.
  !,
  eval(A, Av),                        %% Evaluate sub-expressions.
  eval(B, Bv),
  combine(Op,Av,Bv,Result).           %% Combine sub-expression values

eval(Expr, _) :-		      %% Report error.
  write('unrecognized logical expression: '), 
  write(Expr), nl.

possible_value(0).                    %% Enumerate the two possible values.
possible_value(1).

combine(+, 1, _, 1) :- !.             %% Define binary operators.
combine(+, 0, V, V) :- !.
combine(*, 0, _, 0) :- !.
combine(*, 1, V, V) :- !.
combine(>, 0, _, 1) :- !.
combine(>, 1, V, V) :- !.
combine(=, 0, 0, 1) :- !.
combine(=, 1, 1, 1) :- !.
combine(=, _, _, 0) :- !.

validOp(Op) :- combine(Op, _, _, _).  %% test whether Op is supported.

taut :-                               %% banner, followed by loop
  nl, write('Welcome to taut.'), nl,
  write('Type logical expressions (using !, *, +, >, =) for analysis.'), nl,
  write('Variables must begin with upper-case or _.'), nl,
  write('Enter a period after each expression.'), nl,
  loop.

loop :-                               %% evaluation loop
  read(Expression),
  (Expression \== end_of_file), !,
  analyze(Expression), nl,
  loop.

save :-                               %% save as executable
  save_program(taut, taut).

/* examples, running loop

|: A.
satisfiable, not a tautology

|: A+B.
satisfiable, not a tautology

|: A+!A.
tautology

|: A*!A.
unsatisfiable

|: A>A.
tautology

|: A>(!A>A).
tautology

|: ((A>B)*(B>C))>(A>C).
tautology

|: (A>B)>(!B>!A).
tautology

|: ((A>B)>(A>C))>(B>C).
satisfiable, not a tautology

|: ((A>B)>(A>C))>(C>B).
satisfiable, not a tautology

|: ((A+B)>C)>((A>C)+(B>C)).
tautology

|: (A>(B+C))>((A>B)+(A>C)).
tautology
*/

:- loop.