% ej-1.in
%==============================================================================

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% � Enunciado                                                               %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% S�crates es un hombre. Los hombres son mortales. Luego, S�crates es mortal.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% � Conceptualizaci�n                                                       %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Socrates      S�crates
% Hombre(x)     x es un hombre
% Mortal(x)     x es mortal

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% � Representaci�n                                                          %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

set(auto).

formula_list(usable).
 % 1. S�crates es un hombre
 Hombre(Socrates).

 % 2. Los hombres son mortales.
 all x (Hombre(x) -> Mortal(x)).

 % 3. Luego, S�crates es mortal.
 -Mortal(Socrates).
end_of_list.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% � Demostraci�n                                                            %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% 1 [] -Hombre(x)|Mortal(x).
% 2 [] -Mortal(Socrates).
% 3 [] Hombre(Socrates).
% 4 [hyper,3,1] Mortal(Socrates).
% 5 [binary,4.1,2.1] $F.
