% RA: opuesta.in
% La opuesta de la opuesta con axiomas de igualdad
% 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
 opuesta(derecha) = izquierda.
 opuesta(izquierda) = derecha.
 opuesta(opuesta(derecha)) != derecha.
end_of_list.

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