% RA: paramodulacion.in
% Ejemplo de paramodulación
% Departamento de Ciencias de la Computación e Inteligencia Artificial
% Universidad de Sevilla
% Ref. Genesereth
%==============================================================================


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

set(para_into).
set(para_from).

list(sos).
 P(f(x,b),x) | Q(x).
 f(a,x)=x | R(x).
end_of_list.

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