% RA: Relación 02
% OTTER: puertas.in
% Departamento de Ciencias de la Computación e Inteligencia Artificial
%==============================================================================


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

% En el recinto que se describe en la figura hay una puerta en cada uno de los
% muros. ¿Hay alguna forma de recorrer el recinto, comenzando en el exterior,
% pasando una y sólo una vez por cada una de las puertas y terminando en el
% exterior?.
%
%                      ┏━━━━━━━━━━━   ━━━━━━━━━━━━━┓
%                                                  ┃
%                      ┃                            
%                      ┣━━   ━━━━━━━━┳━━━   ━━━━━━━┫
%                                    ┃              
%                      ┃                           ┃
%                      ┗━━━━━━   ━━━━┻━━━━━━━━   ━━┛

% Utilizar OTTER para encontrar una solución al problema.

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

set(para_into).
set(para_from).
set(hyper_res).

list(demodulators).
 pertenece(x,[])    = $F.
 pertenece(x,[y|w]) = $IF($ID(x,y), $T, pertenece(x,w)).
end_of_list.

formula_list(sos).
 recinto(0,[]) -> recinto(1,[p1]) & recinto(1,[p2]) & recinto(2,[p5]) &
                recinto(2,[p6]) & recinto(3,[p9]) & recinto(3,[p10]) & recinto(3,[p8]).

% Comentarios sobre el ejercicio: La razón por la que el ejercicio no terminaba
% de funcionar correctamente era precisamente la inclusión del literal 'v != w'
% en la siguiente fórmula, junto con la estrategia de hiperresolución. La regla
% de hiperresolución pretende eliminar todos los literales negativos de una
% fórmula para dejar una resolvente únicamente con literales positivos. Si
% observamos la fórmula original:
%   all v w p q z
%       (recinto(v,[p|q]) & recintos(v,z) & recintos(w,z) & distintos(v,w) &
%         -pertenece(z,[p|q]) -> recinto(w,[z,p|q])).
% Cuando se transforma en una cláusula se obtiene:
%   -recinto(v,[x1|x2]) | -recintos(v,z) | -recintos(w,z) |
%   v=w | pertenece(z,[x1|x2]) | recinto(w,[z,x1|x2]).
% Como se puede observar, esta cláusula tiene tres literales negativos y otros
% tres positivos. Por tanto, la estrategia de hiperresolución solo eliminará
% los negativos y dejará los positivos. Es decir, esta estrategia no eliminará
% nunca el literal 'v=w'.
% Por otro lado, la paramodulación utiliza una igualdad de un literal de una
% cláusula dentro de otra y esto no sirve para eliminar el literal 'v=w' de la
% resolvente obtenida.
%
% Una alternativa para evitar el problema consiste en utilizar la estrategia
% 'binary_res' en lugar de 'hyper_res'. Sin embargo esta estrategia es muy
% general y genera multitud de resolventes que están lejos de la solución. El
% proceso de búsqueda de la refutación se hace demasiado largo, y posiblemente
% sin éxito.
%
% Otra alternativa consiste en utilizar un predicado específico para describir
% que dos habitaciones son distintas. Al usar este predicado de forma positiva,
% la hiperresolución sí que podrá eliminarlo adecuadamente. Así es como se ha
% hecho en esta solución.

 all v w p q z
     (recinto(v,[p|q]) & recintos(v,z) & recintos(w,z) & distintos(v,w) &
       -pertenece(z,[p|q]) -> recinto(w,[z,p|q])).

 distintos(0,3).
 distintos(0,2).
 distintos(0,1).
 distintos(1,3).
 distintos(1,2).
 distintos(2,3).
 all x y (distintos(x,y) -> distintos(y,x)).

 recinto(0,[]).
 recintos(0,p1).
 recintos(0,p2).
 recintos(0,p5).
 recintos(0,p6).
 recintos(0,p9).
 recintos(0,p10).
 recintos(0,p8).
 recintos(1,p1).
 recintos(1,p2).
 recintos(1,p3).
 recintos(1,p4).
 recintos(2,p3).
 recintos(2,p5).
 recintos(2,p6).
 recintos(2,p7).
 recintos(3,p8).
 recintos(3,p4).
 recintos(3,p7).
 recintos(3,p9).
 recintos(3,p10).

 all p q (-(recinto(0,[p|q]) & pertenece(p1,[p|q]) & pertenece(p2,[p|q]) &
            pertenece(p3,[p|q]) & pertenece(p4,[p|q]) &
            pertenece(p5,[p|q]) & pertenece(p6,[p|q]) &
            pertenece(p7,[p|q]) & pertenece(p8,[p|q]) &
            pertenece(p9,[p|q]) & pertenece(p10,[p|q]))).

 all x (x = x).
end_of_list.
 
% Como se indicó en clase, el problema no tiene solución y por eso Otter no
% encuentra ninguna prueba. Se puede observar la salida completa y algunos de
% los recorridos que pasan por todas las puertas:
%   recinto(3,[p10,p9,p7,p6,p5,p3,p2,p1,p4,p8]).
%   recinto(3,[p4,p1,p2,p3,p5,p6,p7,p8,p9,p10]).
%   recinto(3,[p10,p9,p7,p6,p8,p4,p3,p5,p2,p1]).
% Al analizar estos recorridos se comprueba que son correctos (pasan por todas
% las puertas una única vez cambiando de habitación), pero que terminan en el
% interior del recinto 3 y no en el exterior (recinto 0) como se pedía en el
% ejercicio.

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