% problem-set/logic.problems/morgan/morgan
% created : 07/15/86
% revised : 07/15/88

% description:
%
% Problem six sent by Charles Morgan of Victoria University:
% Can we deduce from these three axioms alone that       
% (a => b) => [(b => c) => (a => c)], where => means "implies"?

% representaion:
%
% declare_predicate(1,P).
% declare_function(2,i).
% declare_function(1,n).
% declare_constants([a,b,c]).
% declare_variables([x1,x2,x3]).
%
% The axioms are as follows:
%
% 1. P(i(x,i(y,x)))
% 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z))))
% 4. If P(i(x,y)) & P(x) then P(y)
%
% P means "is provable", i means "implies", and n means "not".
% Thus Axiom 4 represents the inference rule of modus ponens.

set(UR_res).

list(axioms).

% axiom 2
P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))).

% axiom 4
-P(i(x1,x2)) | -P(x1) | P(x2).

end_of_list.


list(sos).
 
% axiom 1
P(i(x1,i(x2,x1))).

% negation of hypothesis  
-P(i(i(a,b),i(i(b,c),i(a,c)))).

end_of_list.
