Clase 14 · Inferencia en lógica de primer orden
Pregunta central
¿Cómo puede un agente demostrar una consecuencia cuando su conocimiento contiene objetos, relaciones, variables y cuantificadores? La estrategia de la clase es transformar la base a cláusulas, representar los testigos existenciales mediante símbolos de Skolem y aplicar resolución usando unificación.
Numeración del material
La presentación se titula «Clase 14», aunque el calendario del curso registra el 22 de septiembre como la sesión 13. Este apunte conserva la fecha real y sigue, una por una, las 19 diapositivas del PDF.
Ajuste de continuidad
Este apunte resume la versión completa de 19 diapositivas disponible el 22, pero la nota rápida del 24 de septiembre indica que la clase siguiente retomó el ejercicio de Jack, Curiosity y Tuna. Por eso, las secciones finales siguen siendo correctas como material de estudio, aunque probablemente no describen con exactitud cuánto se alcanzó a cubrir presencialmente el día 22. La versión ampliada del PDF y las discrepancias se documentan en la nota del 24.
Antes de comenzar: cuatro ideas mínimas
La lógica de primer orden representa objetos y relaciones mediante términos y predicados:
- Una constante nombra un objeto: , , .
- Una variable puede representar cualquier objeto del dominio: , , .
- Una función construye un término: o una función de Skolem .
- Un predicado forma una afirmación: , .
Una sustitución reemplaza variables por términos. Por ejemplo, convierte en .
Una cláusula es una disyunción de literales, como:
La cláusula vacía no tiene literales y siempre es falsa. Derivarla significa que las premisas usadas son incompatibles.
Puente con la clase anterior: en resolución proposicional solo se cancelan literales idénticos, como y . En primer orden se pueden cancelar y después de unificarlos con .
Diapositiva 1 · El problema de la inferencia en primer orden
La portada anuncia el tema: inferencia en lógica de primer orden. La representación y la inferencia son tareas diferentes:
- Representar: escribir formalmente hechos y reglas del mundo.
- Inferir: obtener consecuencias que no estaban escritas explícitamente.
Por ejemplo, una base puede contener:
La sentencia no aparece como hecho inicial, pero está vinculada lógicamente por la base. El objetivo de la clase es construir una prueba mecánica de esa consecuencia.
Diapositiva 2 · Agenda: resolución y consecuencia lógica
La diapositiva propone dos temas que deben distinguirse:
- Consecuencia lógica, escrita , es una relación semántica: todo modelo de también satisface .
- Resolución es un procedimiento sintáctico: combina cláusulas para construir una demostración.
La conexión se establece mediante refutación:
undefined\forall x\left( \left[\forall y,(Animal(y)\to Loves(x,y))\right] \to \exists y,Loves(y,x) \right).
### 1. Eliminar implicaciones La implicación exterior $A\to B$ se reemplaza por $\neg A\vee B$ y la interior por $\neg Animal(y)\vee Loves(x,y)$:\forall x\left( \neg\forall y,[\neg Animal(y)\vee Loves(x,y)] \vee\exists y,Loves(y,x) \right).
### 2. Empujar la negación Usamos $\neg\forall y\,P(y)\equiv\exists y\,\neg P(y)$ y De Morgan:\forall x\left( \exists y,[Animal(y)\land\neg Loves(x,y)] \vee\exists y,Loves(y,x) \right).
### 3. Estandarizar variables Los dos cuantificadores existenciales son independientes. Renombramos el segundo $y$ como $z$:\forall x\left( \exists y,[Animal(y)\land\neg Loves(x,y)] \vee\exists z,Loves(z,x) \right).
Cambiar el nombre de una variable ligada no cambia el significado; evita confundir dos testigos potencialmente distintos. ## Diapositiva 7 · Conversión trabajada, parte II ### 4. Skolemizar Ambos existenciales aparecen bajo el alcance de $\forall x$, por lo que sus testigos pueden depender de $x$. Introducimos dos funciones diferentes: $$y:=F(x),\qquad z:=G(x).$$ La fórmula se convierte en:\forall x\left( [Animal(F(x))\land\neg Loves(x,F(x))] \vee Loves(G(x),x) \right).
undefined\forall x\left( [Animal(F(x))\vee Loves(G(x),x)] \land [\neg Loves(x,F(x))\vee Loves(G(x),x)] \right).
### 6. Omitir el universal y separar cláusulas\begin{aligned} A_1&: Animal(F(x))\vee Loves(G(x),x),\ A_2&: \neg Loves(x,F(x))\vee Loves(G(x),x). \end{aligned}
Estas dos cláusulas son equisatisfactibles con la fórmula de partida y ya pueden alimentar el algoritmo de resolución. ## Diapositiva 8 · Regla de resolución con unificación Sean dos cláusulas con literales $p$ y $\neg q$. Si $p$ y $q$ admiten un unificador $\theta$, la regla es:\frac{f_1\vee\cdots\vee f_n\vee p,qquad \neg q\vee g_1\vee\cdots\vee g_m} {Subst!\left(\theta, f_1\vee\cdots\vee f_n\vee g_1\vee\cdots\vee g_m\right)}, \qquad \theta=Unify(p,q).
undefined\forall x,[Humano(x)\to Mortal(x)],qquad Humano(Sócrates).
Para una prueba por refutación se añade la negación de la consulta: $$\neg Mortal(Sócrates).$$ La tercera fórmula no es un hecho que creamos verdadero; es una hipótesis provisional que intentaremos volver incompatible con la base. ## Diapositiva 10 · Ejercicio de Sócrates: pasar a cláusulas Solo la primera fórmula necesita transformación:\forall x,[Humano(x)\to Mortal(x)] \equiv \forall x,[\neg Humano(x)\vee Mortal(x)].
Al omitir el universal, el conjunto de cláusulas es: | Nº | Cláusula | Tipo | |---:|---|---| | 1 | $\neg Humano(x)\vee Mortal(x)$ | Regla universal | | 2 | $Humano(Sócrates)$ | Hecho | | 3 | $\neg Mortal(Sócrates)$ | Negación de la consulta | No hace falta skolemizar porque no existen cuantificadores existenciales. ## Diapositiva 11 · Ejercicio de Sócrates: cerrar la refutación Primer paso: resolver 1 y 2. $Humano(x)$ unifica con $Humano(Sócrates)$ mediante $\theta=\{x/Sócrates\}$:\frac{\neg Humano(x)\vee Mortal(x),\quad Humano(Sócrates)} {Mortal(Sócrates)}.
\frac{Mortal(Sócrates),\quad\neg Mortal(Sócrates)}{\square}.
undefined\begin{aligned} A:;&\forall x\left( [\forall y,(Animal(y)\to Loves(x,y))] \to[\exists y,Loves(y,x)] \right),\ B:;&\forall x\left( [\exists z,(Animal(z)\land Kills(x,z))] \to[\forall y,\neg Loves(y,x)] \right),\ C:;&\forall x,[Animal(x)\to Loves(Jack,x)],\ D:;&Kills(Jack,Tuna)\vee Kills(Curiosity,Tuna),\ E:;&Cat(Tuna),\ F:;&\forall x,[Cat(x)\to Animal(x)]. \end{aligned}
La consulta es: $$G: Kills(Curiosity,Tuna).$$ Para refutar su negación añadimos: $$\neg G:\quad\neg Kills(Curiosity,Tuna).$$ > [!note] Cambio de letras entre diapositivas > > En la diapositiva 12 la pregunta aparece como inciso E. En la formalización se añaden los hechos sobre Tuna como E y F, por lo que la consulta pasa a llamarse G. Es solo un cambio de etiquetas. ### Comprobación del alcance En A, «ama a todos los animales» forma el antecedente completo de la implicación. En B, el $z$ existencial representa algún animal asesinado y el $y$ universal expresa que ninguna persona ama al asesino. Los paréntesis son esenciales: mover un cuantificador fuera de su alcance puede cambiar el significado. ## Diapositiva 14 · Toda la base en CNF La fórmula A produce las dos cláusulas derivadas en las diapositivas 6–7:\begin{aligned} A_1:;&Animal(F(x))\vee Loves(G(x),x),\ A_2:;&\neg Loves(x,F(x))\vee Loves(G(x),x). \end{aligned}
\begin{aligned} &\forall x\left( [\exists z,(Animal(z)\land Kills(x,z))] \to[\forall y,\neg Loves(y,x)] \right)\ &\equiv \forall x\left( \neg\exists z,[Animal(z)\land Kills(x,z)] \vee\forall y,\neg Loves(y,x) \right)\ &\equiv \forall x\forall z\forall y,[ \neg Animal(z)\vee\neg Kills(x,z)\vee\neg Loves(y,x) ]. \end{aligned}
undefinedA_2:\ \neg Loves(Jack,F(Jack))\vee Loves(G(Jack),Jack)
C:\ \neg Animal(F(Jack))\vee Loves(Jack,F(Jack)).
undefined