%==============================================================================
% Enunciado
%==============================================================================

%   Formalizar en Otter la siguiente argumentación: ``Sólo las buenas personas
% ayudan a los pobres. Ninguna buena persona es aficionada a la fotografía.
% Antonio ayuda a Juan y es aficionado a la fotografía. Luego Juan no es
% pobre.''

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

% Lenguaje del problema

% BP(X) : X es buena persona.
% P(X) : X es pobre.
% F(X) : X es aficionado a la fotografía.
% A(X,Y) : X ayuda a Y.
% Juan, Antonio

set(auto2).

formula_list(sos).
  all x y (A(x,y) & P(y) -> BP(x)).
  all x (F(x) -> -BP(x)).
  A(Antonio,Juan) & F(Antonio).
  P(Juan).
end_of_list.

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