% RA: edificio.in
% Un edificio de tres plantas
% 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 un edificio de tres plantas viven Daniel, Jaime y Andrés. Todos los
% habitantes de la primera planta conocen a todos los de la tercera. Jaime sólo
% conoce a habitantes de la segunda y la tercera plantas. Andrés no vive en la
% segunda planta y no conoce a nadie de la tercera planta. Jaime vive en la
% segunda planta y conoce a Daniel. Por tanto Daniel vive en la segunda
% planta."

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

% Configuración del sistema

set(auto2).

% Lenguaje del problema

% Constantes:

% Propiedades:

% Relaciones:

% Formalización:

formula_list(sos).
  all x (primera(x) | segunda(x) | tercera(x)).
  all x y (primera(x) & tercera(y) -> conoce(x,y)).
  all x (conoce(Jaime,x) -> ( segunda(x) | tercera(x)) ).
  - segunda(Andres).
  all x (tercera(x) -> -conoce(Andres,x)).
  segunda(Jaime) & conoce(Jaime,Daniel).

  all x (conoce(x,x)).
  - segunda(Daniel).
end_of_list.

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