Nociones de Lógica

Figura 6.1: Las dos caras de la Lógica.
\begin{figure}\centerline{\hbox{
\psfig{figure=logica.ps,height=6cm}
}}\end{figure}

Importante: que las cosas que queremos que sean verdaderas coicidan con las que podemos probar.

Osea: lo que nos implica la teoría es lo que podemos computar.

Características:

Un alfabeto consiste de variables (aquí la primera letra en mayúscula), símbolos de predicados y de funciones (la primera letra en minúscula).

Términos = Funciones (símbolo funcional + argumentos) y Variables.

Un predicado (símbolo + argumentos) es una fórmula atómica o simplemente un átomo.

válido inválido
     
siempre cierto a veces T o F siempre falso
     
satisfacible insatisfacible

Una fórmula $G$ se dice que es una consequencia lógica de un conjunto de fórmulas $F = \{F_1, \ldots, F_n\}, N \geq 1$, denotado por $F \models G$ si para cada interpretación $w$ para la cual $w(F_1
\wedge F_2 \wedge \ldots F_n) = true$, entonces $w(G) = true$

Satisfacibilidad, valides, equivalencia y consecuencia lógica son nociones semánticas (generalmente establecidas por medio de tablas de verdad).

Para derivar consecuencias lógicas también se pueden hacer por medio de operaciones exclusivamente sintáctivas (e.g., modus ponens, modus tollens).

Las cláusulas, son la forma utilizada en prueba de teoremas y programación lógica.

Una literal: un átomo o su negación

Una clásula: es una fórmula cerrada de la forma:

\begin{displaymath}\forall X_1 \ldots \forall X_s (L_1 \vee \ldots \vee L_m) \end{displaymath}

donde cada $L_i$ es una literal y las $X_i$ son todas las variables que aparecen en las literales.

Equivalencias:

\begin{displaymath}\forall x_1 \ldots \forall x_s (A_1 \vee \ldots A_n \vee \neg B_1
\ldots \vee \neg B_m) \equiv \end{displaymath}


\begin{displaymath}\forall x_1 \ldots \forall x_s ( B_1 \wedge \ldots \wedge B_m
\rightarrow A_1 \vee \ldots A_n) \end{displaymath}

Se escribe normalmente como:

\begin{displaymath}A_1, \ldots, A_n \leftarrow B_1, \ldots B_m \end{displaymath}

Una cláusula de Horn: a lo más una literal positiva.

\fbox{
\begin{minipage}{5cm}
\begin{tabbing}
123465\= \kill
\> $A$\ \= $\leftarr...
...ldots, B_n$\ \\
\> $A \leftarrow B_1, \ldots, B_n$
\end{tabbing}\end{minipage}}

Una cláusula definitiva (definite clause) es una cláusula con una literal positiva ($A \leftarrow$ o $A \leftarrow
B_1, \ldots, B_n$).

Razonamiento en lógica: reglas de inferencia

Estas reglas solo hacen manipulación sintáctica (son formas procedurales).

Lo interesante es ver como las formas procedurales semánticas están relacionadas con las sintácticas.

Una regla de inferencia es robusta/válida (sound) si $S \vdash
F$ entonces $S \models F$.

Osea una colección de reglas de inferencia es válida si preserva la noción de verdad bajo las operaciones de derivación.

Una regla de inferencia es completa (complete) si $S \models F$ entonces $S \vdash F$.

Resolución

Resolución solo sirve para fórmulas en forma de cláusulas.

Idea: prueba por refutación

Para probar: $P \vdash Q$, hacer $W = P \cup \{ \neg Q\}$ y probar que $W$ es insatisfacible

Ejemplo sencillo:

Sean $C_1$ y $C_2$ dos cláusulas con literales $L_1$ y $L_2$ (donde $L_1$ y $L_2$ son complementarias). La resolución de $C_1$ y $C_2$ produce: $C = C_1' \cup C_2'$ donde: $C_1' = C_1 - \{L_1\}$ y $C_2' = C_2 - \{L_2\}$ (eliminando literales redundantes)

Figura 6.2: Un árbol de derivación proposicional.
\begin{figure}\centerline{\hbox{
\psfig{figure=resolucion1.ps,height=6cm}
}}\end{figure}

Para lógica de primer orden: substitución y unificación.

Una substitución $\Theta = \{ X_1/t_1, \ldots, X_k/t_k\}$ es una función de variables a términos. La aplicación $W\Theta$ de una substitución $\Theta$ a una wff $W$ se obtiene al reemplazar todas las ocurrencias de cada variable $X_j$ por el mismo término $t_j$.

Al aplicar una substitución a una wff se genera una nueva expresión (una instancia).

Una substitución $\sigma$ es un unificador de un conjunto de expresiones $\{E_1, \ldots, E_m\}$ si $E_1\sigma = \ldots = E_m\sigma$

Un unificador $\theta$, es el unificador más general (mgu) de un conjunto de expresiones $E$, si para cada unificador $\sigma$ de $E$, existe una substitución $\lambda$ tal que $\sigma
= \theta \lambda$

Para hacer resolución en lógica de primer orden tenemos que comparar si dos literales complementarias unifican. El algoritmo de unificación construye un mgu de un conjunto de expresiones.

Sean $C_1$ y $C_2$ dos cláusulas con literales $L_1$ y $L_2$ respectivamente. Si $L_1$ y $\neg L_2$ tienen un mgu $\sigma$, el resolvente de $C_1$ y $C_2$ es la cláusula: $(C_1 \sigma
- \{L_1 \sigma\}) \cup (C_2 \sigma - \{L_2 \sigma\})$ (ver figura 6.3).

El algoritmo de unificación no es determinístico (se pueden seleccionar las cláusulas de varias formas).

Figura 6.3: Un árbol de derivación lineal de primer orden.
\begin{figure}\centerline{\hbox{
\psfig{figure=resolucion2.ps,height=6cm}
}}\end{figure}

Existen diferentes estrategias de resolución, e.g., semántica, lineal, SLD, etc., para restringir el número de posibles cláusulas redundantes.

Resolución SLD

Seleccionar una literal, usando una estrategia Lineal, restringido a cláusulas Definitivas.

Resolución lineal:

Una forma especial de resolución lineal es: input resolution. En esta estrategia, cada paso de resolución, exceptuando el primero, se toma del último resolvente (cláusulas metas) y del conjunto original (cláusulas de entrada).

Input resolution es completa para cláusulas de Horn, pero no para cláusulas en general.

Una variante de input resolution es resolución SLD para cláusulas de Horn. Resolución de entrada se extiende con una regla de selección que determina en cada paso que literal de la cláusula meta es seleccionada.

La estrategia de búsqueda afecta el resultado.

Aunque resolución SLD es sound y refutation complete para cláusulas de Horn, en la práctica (por razones de eficiencia) se hacen simplificaciones:

Esto es lo que usa básicamente PROLOG

emorales 2012-01-23