% RA: japones.in
% Juan conoce a alguien a quien le gusta la comida asiática
% Departamento de Ciencias de la Computación e Inteligencia Artificial
% Universidad de Sevilla
%==============================================================================


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

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "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. Juan no conoce a todos los que trabajan en su oficina. Por tanto,
% Juan conoce a alguien a quien le gusta la comida asiática."

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

% Configuración del sistema

set(auto2).

% Lenguaje del problema
% Nota: Identificamos comida Japonesa y comida Asiática

% Constantes:
%  Juan

% Propiedades:

% Relaciones:

formula_list(sos).
  exists x (oficina(x,Juan) & comidaInternacional(x)).
  all x (comidaJaponesa(x) -> conoce(Juan,x)).
  exists x (oficina(x,Juan) & -conoce(Juan,x)).
  
  % all x (comidaInternacional(x) -> comidaJaponesa(x)).
  all x (comidaInternacional(x) -> comidaAsiatica(x)).
  all x (comidaAsiatica(x) -> comidaJaponesa(x)).
  all x y (oficina(x,y) -> oficina(y,x)).

  % all x (-conoce(Juan,x) | -comidaJaponesa(x)).
  % -(exists x (conoce(Juan,x) & comidaJaponesa(x))).
  all x (-conoce(Juan,x) | -comidaAsiatica(x)).
end_of_list.

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