% RA: conduccion.in
% El mejor conductor del mundo
% 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:
% "Para todo hombre hay una mujer que no conduce peor que él, por tanto el
% mejor conductor del mundo es una mujer."

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

% Configuración del sistema

set(auto2).

% Lenguaje del problema

% Propiedades:

% Relaciones:

formula_list(sos).
  all x (hombre(x) -> (exists y (mujer(y) & -conducePeor(y,x)))).
  
  - (exists y (mujer(y) & (all x (-conducePeor(y,x))))).

  % Existe 'el mejor conductor del mundo'
  exists y (all x (-conducePeor(y,x))).

  % Aquí estaba el error: La transitividad se necesita para la relación
  % '-conducePeor', no para la relación 'conducePeor'
  all x y z (-conducePeor(x,y) & -conducePeor(y,z) -> -conducePeor(x,z)).
  all x y (conducePeor(x,y) -> -conducePeor(y,x)).
  all x (-conducePeor(x,x)).
  all x (hombre(x) | mujer(x)).
end_of_list.

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