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

%   Formalizar en Otter la siguiente argumentación: ``En la oficina de Juan
% hay personas a las que le gusta la comida internacional. De hecho, Juan
% conoce a todos a los que le gusta la comida japonesa. Por tanto, Juan conoce
% a alguien a quien le gusta la comida asiática.''

%   Comprobar si la argumentación es válida y, en caso de que lo sea, obtener
% una prueba lo más corta posible de la misma.

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

% Lenguaje del problema

% Asiatica(X) : A X le gusta la comida asiática.
% Japonesa(X) : A X le gusta la comida japonesa.
% Internacional(X) : A X le gusta la comida internacional.
% conocido(X) : Juan conoce a X.

set(auto2).

formula_list(sos).
  all x (asiatica(x) -> japonesa(x)).
  all x (internacional(x) -> asiatica(x)).
  all x (japonesa(x) -> conocido(x)).
  exists x (internacional(x)).
  exists x (-conocido(x)).
  % exists x (asiatica(x) & conocido(x)).
  all x (-asiatica(x) | -conocido(x)).
end_of_list.

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