% RA: gripe.in
% La gripe se contagia irremediablemente en el trabajo
% 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:
% "Alberto y Juan trabajan juntos. Juan trabaja con todos los comerciales. La
% gripe se contagia irremediablemente en el trabajo. Hay un comercial
% contagiado de gripe. Por tanto, Alberto tiene la gripe."

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

% Configuración del sistema

set(auto2).

% Lenguaje del problema

% Constantes:

% Propiedades:

% Relaciones:

formula_list(sos).
  trabajan(Alberto,Juan).
  all x (comercial(x) -> trabajan(Juan,x)).
  all x y (gripe(x) & trabajan(x,y) -> gripe(y)).
  exists x (comercial(x) & gripe(x)).
  -gripe(Alberto).

  all x y (trabajan(x,y) -> trabajan(y,x)).
  all x y z (trabajan(x,y) & trabajan(y,z) -> trabajan(x,z)).
end_of_list.

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