% RA: mayor.in
% El padre es mayor que el hijo con axiomas de igualdad y resolución binaria
% Departamento de Ciencias de la Computación e Inteligencia Artificial
% Universidad de Sevilla
%==============================================================================


%==============================================================================
% Formalización
%==============================================================================

set(binary_res).

list(sos).
 x=x.                                   % Reflexividad
 x!=y | y=x.                            % Simetría
 x!=y | y!=z | x=z.                     % Transisitividad
 x!=y | Padre(x)=Padre(y).              % Sustitución
 x1!=x2 | -Mayor(x1,y) | Mayor(x2,y).   % Sustitución
 y1!=y2 | -Mayor(x,y1) | Mayor(x,y2).   % Sustitución
 Mayor(Padre(x),x).
 Padre(Juan)=Luis.
 -Mayor(Luis,Juan).
end_of_list.

%==============================================================================
