% RA: ayuda.in
% Antonio ayuda a todos los que trabajan en su oficina
% 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:
% "Todos los que ayudan a Juan viven en casa de Manolo. Antonio ayuda a todos
% los que trabajan en su oficina. Todos los amigos de Carlos trabajan en la
% misma oficina que Miguel. Carlos es amigo de Antonio y Miguel trabaja con
% Juan. Por tanto, Antonio vive en casa de Manolo."

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

% Configuración del sistema

set(auto2).

% Lenguaje del problema

% Constantes:

% Propiedades:

% Relaciones:

formula_list(sos).
  all x (ayuda(x,Juan) -> vive(x,Manolo)).
  all x (trabaja(x,Antonio) -> ayuda(Antonio,x)).
  all x (amigo(x,Carlos) -> trabaja(x,Miguel)).
  amigo(Carlos,Antonio).
  trabaja(Miguel,Juan).
  -vive(Antonio,Manolo).
end_of_list.

formula_list(usable).
  all x y (vive(x,y) -> vive(y,x)).
  all x y (trabaja(x,y) -> trabaja(y,x)).
  all x y (amigo(x,y) -> amigo(y,x)).
  all x y z (vive(x,y) & vive(y,z) -> vive(x,z)).
  all x y z (trabaja(x,y) & trabaja(y,z) -> trabaja(x,z)).
end_of_list.

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