\documentstyle{article}
\setlength{\textheight}{25cm}
\setlength{\headsep}{0cm}
\setlength{\oddsidemargin}{-.55in}
\setlength{\textwidth}{18cm}
\setlength{\linewidth}{18cm}
\pretolerance=10000
\tolerance=10000
\begin{document}
\pagestyle{empty}
\centerline{\Large \bf  Febrero 1998 (MD 2)}
\vspace{0.25cm}
\small 
\begin{enumerate}

\item Encontrar el n\'umero de soluciones enteras de la siguiente
 ecuaci\'on: $$x+y+z+t+u=14$$ donde  $0 \leq x,\, u; \; 2 \leq y,\,z,\, t .$
 
 Utilizando este resultado (o de otra forma) calcular cu\'antos subconjuntos de cuatro
 elementos tiene $C=\{1,2,3,\dots ,15\}$ que no contengan enteros consecutivos.
  Subconjuntos como por ejemplo: $\{1,3,7,10\}$ o $\{2,5,11,15\}.$
 
\item Una permutaci\'on $\sigma$ de $n$ elementos se llama {\em desarreglo} si no tiene ning\'un
punto fijo (i.e. $\sigma(i)\neq i \; \forall i=1..n.$) Denotando $D(n)$ el n\'umero
de desarreglos de $n$ objetos, demostrar que:
$$n!=\sum _{k=0}^{n}{n\choose k} D(k).$$
 
\item Describir el uso de las funciones generatrices para resolver recurrencias.  
Dar una justificaci\'on del m\'etodo.
	  
\item  Definimos un {\em abanico} de orden $n$ como un grafo de v\'ertices $\{0,1,
\dots , n\}$ con $2n-1$ ejes definidos por: El v\'ertice $0$ se conecta,
mediante un eje, con cada uno de los
otros v\'ertices, y el v\'ertice $k$ se conecta mediante un eje con el v\'ertice
$k+1$ para todo $k, \; 1 \leq k < n.$ 

Calcular el n\'umero de \'arboles de recubrimiento ({\em spanning trees}) que posee un
abanico de orden $n.$ Justificar la respuesta.

\item Describe como se representa la l\'ogica de orden superior en el systema HOL.
Describe los t\'erminos y los tipos. Justifica la necesidad del tipado con alg\'un
ejemplo.

\item Describe las tres reglas de inferencia primitivas de HOL ASSUME (introducci\'on
de hip\'otesis), DISCH (eliminaci\'on de hip\'otesis) y MP (modus ponens).

  La funci\'on \verb"dest_thm" descompone un teorema en un par formado por una
  lista de hip\'otesis y una conclusi\'on. El tipo \verb"goal" es una abreviatura
  de \verb"(term)list # term".
 
Consideremos la siguiente sesi\'on en Hol88: 
\begin{verbatim}
#let Th3 = ASSUME "t1==>t2";;
Th3 = . |- t1 ==> t2
#dest_thm Th3;;
["t1 ==> t2"],"t1 ==> t2" : goal 
#let Th4 = DISCH "t1==>t2" Th3;;
Th4 = |- (t1 ==> t2) ==> t1 ==> t2 
#let Th5 = ASSUME "t1:bool";;
Th5 = . |- t1
#let Th6 = MP Th3 Th5;;
Th6 = .. |- t2
\end{verbatim} 
Las hip\'otesis de \verb"Th6"  pueden inspeccionarse con la funci\'on
 \verb"hyp", quer devuelve la lista de hip\'otesis de un theorema.
\begin{verbatim}
#hyp Th6;;
["t1 ==> t2"; "t1"] : term list
\end{verbatim}
Se puede hacer que HOL imprima todas las hip\'otesis explicitamente usando la
funci\'on \verb"print_all_thm" en lugar de la por defecto \verb"print_thm." 
\begin{verbatim}
#top_print print_all_thm;;
- : (thm -> void)
#Th5;;
t1 |- t1
#Th6;;
t1 ==> t2, t1 |- t2 
#let Th7 = DISCH "t1==>t2" Th6;;
Th7 = t1 |- (t1 ==> t2) ==> t2
#let Th8 = DISCH "t1:bool" Th7;;
Th8 = |- t1 ==> (t1 ==> t2) ==> t2
\end{verbatim}
Describe cada uno de los pasos de la sesi\'on. La sucesi\'on de teoremas 
 \verb"Th3, Th5, Th6, Th7, Th8" constituye una prueba en HOL. 
 ?`De qu\'e teorema?.

Escribir la sesi\'on anteror en notaci\'on l\'ogica est\'andar.
 
	 
\end{enumerate}

 
\end{document}