prolog 2

logica_predicados.tex

@@ -323,8 +323,35 @@ Ahora si ya estamos en esa estructura y ese modelo ¿qué podemos decir de las s
 \end{align*}
 
 %\section*{Sustitución}
+Venaos un poco las definiciones para ver si queda más claro el tema.
 
+\begin{defi}
+  Dado un lenguaje de primer orden $\mathbf{L}$, una $\mathbf{L}$-estructura (o simplemente una estructura) $\mathbf{M}$ es una pareja $\mathbf{M}= \{ M,I \}$ donde $M$ es un conjunto no vacío llamado el dominio de la estructura e $I$ es una función llamada \emph{función de interpretación} que asigna funciones y predicados en $M$ a los símbolos $\mathbf{L}$ de acuerdo a:
 
+  \begin{itemize}
+  \item Para todo símbolo función $f$ de rango $n>0$, $I(f): M^n\rightarrow M$, o $f_M$, es una función n-aria.
+  \item Para toda constante $c$, $I(c)$, o $c_M$, es un elemento de $M$
+    \item Para todo símbolo predicado $P$ de rango $n\geq 0$, $I(P): M^n \rightarrow BOOL$, o $P_M$,  es un predicado n-ario. En particular, los símbolos predicados de rango $0$ son interpŕetados como valores de verdad.
+  \end{itemize}
+\end{defi}
+
+Esto es un tanto abstracto, pero lo que sucede es que podemos definir un lenguaje de primer orden, pero también debemos darle sentido a lo que hacemos, para eso necesitamos de una estructura en la que podamos evaluar los términos. Tal como los ejemplos de las combinaciones de sabores de helado, podemos tener el lenguaje para armarlos, pero sólo bajo la estructura de helado (que por lo regular es frío y de sabor dulce) es que tienen sentido sólo ciertas combinaciones de sabores. Ahora veamos como es que evaluamos los términos de acuerdo a este formalismo.
+
+\begin{defi}
+  Dado un lenguaje $\mathbf{L}$ de primer orden y una $\mathbf{L}$-estructura $\mathbf{M}$, una asignación es una función $s: \mathbf{V}\rightarrow M$ del conjunto de variables $\mathbf{V}$ al dominio $M$. El conjunto de todas esa funciones lo escribimos como $[\mathbf{V}\rightarrow M]$ 
+\end{defi}
+
+Asignamos un valor para eventualmente tener una respuesta de verdadero o falso, el significado de una fórmula es una función de esta asignación a los booleanos, entonces el conjunto de todas las funciones se convierte en $[[\mathbf{V}\rightarrow M]\rightarrow BOOL]$.
+
+Para tratar de que quede más claro veamos un ejemplo.
+
+\textbf{Ejemplo:} Sea el lenguaje de primer orden $\mathbf{L}= \{=, \leq, +,*,0,1\}$, una interpretación de este lenguaje es:
+
+\begin{equation*}
+  M = \{\mathbb{N}, =, \leq, +, * ...,0,1\},
+\end{equation*}
+
+\noindent donde $\mathbb{N}$ es el conjunto de los números naturales, ``$=$'' es la relación de igualdad en sobre el mismo conjunto, $\leq$ la relación ``mnor o igual'' sobre los naturales, y ``$+$'' y ``$+$'' son la suma y multiplicación en $\mathbb{N}$ respectivamente. 
 
 \newtheorem{teo}{Teorema}
 \begin{teo}

progra_log.tex

@@ -70,43 +70,41 @@ Ya empezamos a ver que poder determinar si dos términos son unificables puede s
 
 Los términos son vistos como árboles aumentados.
 
-\begin{multicols}{2}
-  \begin{figure}
-    \begin{center}
-      \begin{tikzpicture}
-        [
-          level 1/.style = {sibling distance = 0.7cm, level distance = 0.8cm}
-        ] 
-        \node {k}
-        child {node {g}
-          child {node {x}}
-          child {node {y}}}
-        child {node {a}};
+\begin{figure}
+  \begin{center}
+    \begin{tikzpicture}
+      [
+        level 1/.style = {sibling distance = 0.7cm, level distance = 0.8cm}
+      ] 
+      \node {k}
+      child {node {g}
+        child {node {x}}
+        child {node {y}}}
+      child {node {a}};
  
-      \end{tikzpicture}
-      \caption{Árbol para el algoritmo no determinista de Robinson para el término $k(g(x,y),a)$}
-      \label{fig:tree1}
-    \end{center}
-  \end{figure}
+    \end{tikzpicture}
+    \caption{Árbol para el algoritmo no determinista de Robinson para el término $k(g(x,y),a)$}
+    \label{fig:tree1}
+  \end{center}
+\end{figure}
 
-  \begin{figure}
-    \begin{center}
-      \begin{tikzpicture}
-        [
-          level 1/.style = {sibling distance = 0.7cm, level distance = 0.8cm}
-        ] 
-        \node {k}
-        child {node {g,1}
-          child {node {x,1}}
-          child {node {y,2}}}
-        child {node {a,2}};
+\begin{figure}
+  \begin{center}
+    \begin{tikzpicture}
+      [
+        level 1/.style = {sibling distance = 0.7cm, level distance = 0.8cm}
+      ] 
+      \node {k}
+      child {node {g,1}
+        child {node {x,1}}
+        child {node {y,2}}}
+      child {node {a,2}};
  
-      \end{tikzpicture}
-      \caption{Árbol aumentado para el algoritmo no determinista de Robinson}
-      \label{fig:tree1}
-    \end{center}
-  \end{figure}
-\end{multicols}
+    \end{tikzpicture}
+    \caption{Árbol aumentado para el algoritmo no determinista de Robinson}
+    \label{fig:tree2}
+  \end{center}
+\end{figure}
 
 \begin{itemize}
 \item El árbol asociado a una variable tiene un sólo nodo, el de la variable en sí
@@ -118,7 +116,7 @@ Se aumenta el árbol indicando el número de hijo que es del nodo padre (en el o
 
 Supongamos que tenemos el término $w$ con ocurrencia en $s$ y $u$ con ocurrencia en $t$, el par $w,u$ son un \emph{par en desacuerdo} si sus caminos de acceso difieren sólo por la etiqueta del último nodo.
 
-Un par es simple si uno de ellos es una variable que ocurre en el otro término.
+Un par es simple si uno de ellos \textbf{no} es una variable que ocurre en el otro término.
 
 \begin{lema} 
   (\textbf{Desacuerdo}) Sean $u$ y $w$ un par en desacuerdo de $s$ y $t$:
@@ -142,4 +140,71 @@ Ahora sí el algoritmo de unificación de Robinson:
 
 Vamos a ampliar el algoritmo.
 
+\subsection{Algoritmo de Robinson}
+
+Para ampliarlo ahora se buscarán los pares en desacuerdo en cierto orden. Para ello no necesitaremos de la estructura de árbol, ya que el orden que daremos para la búsqueda de los pares será el orden textual, la forma de leer el término, de izquierda a derecha.
+
+\begin{itemize}
+\item Sea $\theta$ igual a $\epsilon$
+  \item iniciamos la lectura en los primeros símbolos a la izquierda de $s\theta$ y $t\theta$
+\item Mientras $s\theta \neq t\theta$ repite:
+  \begin{itemize}
+  \item Avanza de manera simultanea a la derecha hasta que un par de símbolos diferentes en $s\theta$ y $t\theta$ sean encontrados.
+  \item Determina el par de términos $w$ y $u$ cuyos símbolos iniciales son los identificados y realiza las acciones asociadas:
+    \begin{itemize}
+    \item $u$ y $w$ son un par simple $\implies$ sea $\gamma$ una sustitución dada por $u$ y $w$, sea $\theta = \theta \gamma$
+    \item $u$ y $w$ no son un pare simple $\implies$ detente como fallo.
+    \end{itemize}
+  \end{itemize}
+\end{itemize}
+
+\textbf{Ejemplo:} Sea el par de términos:
+
+\begin{align*}
+  &k(z,f(x,b,z))\\
+  &k(h(x), f(g(a),y,z))
+\end{align*}
+
+Primer par en desacuerdo: $z$, $h(x)$. Este par define la sustitución $\{z/h(x)\}$, aplicándola:
+
+\begin{align*}
+  &k(h(x),f(x,b,h(x)))\\
+  &k(h(x), f(g(a),y,h(x)))
+\end{align*}
+
+El siguiente par en desacuerdo: $x$, $g(a)$. Esto define la sustitución $\{x/g(a)\}$, aplicando:
+
+\begin{align*}
+  &k(h(g(a)),f(g(a),b,h(g(a))))\\
+  &k(h(g(a)), f(g(a),y,h(g(a))))
+\end{align*}
+
+El siguiente par en desacuerdo: $b$, $y$. Esto define la sustitución $\{y/b\}$, aplicando:
+
+\begin{align*}
+  &k(h(g(a)),f(g(a),b,h(g(a))))\\
+  &k(h(g(a)), f(g(a),b,h(g(a))))
+\end{align*}
+
+Ya son términos idénticos, las sustituciones que forma el umg son $\{z/h(x)\{x/g(a)\}\{y/b\} = \{z/h(g(a)), x/g(a), y/b\}$. 
+
+\section{Clausulas definidas}
+
+\begin{defi}
+  Una clausula definida es un enunciado de la forma
+  \begin{equation*}
+    \forall x_1,...,x_m.(\exists y_1,...,y_k.(\beta_1\wedge \cdots \wedge \beta_n))\implies \alpha
+  \end{equation*}
+  \noindent donde $\beta_1,...,\beta_n$ y $\alpha$ son fórmulas atómicas y dependen de las variables $y_1,...,y_k$ y $x_1,...,x_m$ respectivamente, pero no comparten esa dependencia. Está clausula se escribirá como
+
+  \begin{equation*}
+    \alpha \leftarrow \beta_1,...,\beta_n
+  \end{equation*}
+  \begin{itemize}
+  \item $\alpha$ es el encabezado y $\beta_1,..,\beta_n$ el cuerpo.
+  \item Una fórmula puede carecer de cuerpo o encabezado. Si no tiene encabezado es una \textbf{meta}.
+  \item Un programa lógico es un conjunto de clausulas definidas, ninguna de las cuales es una meta.
+  \end{itemize}
+\end{defi}
+
 \end{document}