Lógica de predicados

Lógicas y métodos formales Comentarios desactivados en Lógica de predicados

La lógica proposicional falla cuando desaeamos expresar cosas como todos..., sólo..., existe... La lógica de predicados, o lógica de primer orden, incluye los conceptos de predicado, variable y cuantificadores para poder representar con mayor exactitud enunciados declarativos, extendiendo así la lógica proposicional. Los predicados representan propiedades que son ciertas y se representan con letras mayúsculas, $latex P, Q, R, \ldots$ Las variables son los conceptos que recojen valores concretos y se representan con letras minúsculas $latex x, y, z, \ldots$ Las variables pueden ser cuantificadas usando los cuantificadores universal $latex \forall$ y existencial $latex \exists$, que se leen "para todo" y "existe" respectivamente.

Por ejemplo, para expresar el típico enunciado lógico (y políticamente correcto ;-) "Los humanos son mortales" necesitamos dos predicados:

$latex H(x): x$ es un humano

$latex M(x): x$ es mortal.

Y con ellos podemos construir el enunciado

$latex \forall x(H(x) \to M(x))$

que se leería "para todo x, si x es humano entonces x es mortal".

Además de los símbolos de predicado, es posbible emplear otros símbolos adicionales, llamados funciones, que permiten escribir expresiones más compactas y más sencillas de comprender. Las funciones se representan mediante letras minúsculas. Por ejemplo, el predicado $latex M(x,y)$ significa que $latex x$ es la madre de $latex y$. Pero realmente estamos diciendo que $latex x$ es una de las madres de $latex y$, lo cual no es muy elegante porque sabemos que una persona sólo puede tener una madre (biológica). En ese caso, puede emplearse un símbolo de función $latex m(x)$ para representar a la madre de $latex x$. Veamos la diferencia. Las dos expresiones siguientes:

$latex \forall x \forall y (H(x) \land M(x,y) \to J(x,y))$

$latex \forall x (H(x) \to J(x, m(x)))$

se leen igual: un hijo -H(x)- es más joven -J(x,y)- que su madre -M(x,y) o m(x)-.

Esta representación es válida sólo para denotar un único objeto; no podría usarse, por ejemplo, para representar el concepto de "hermano". H(x) es un predicado unario (sólo tiene un argumento) y J(x,y) es un predicado binario. En general, los predicados (y también las funciones) pueden tener n argumentos. Al número de argumentos se le denomina aridad.

Las reglas de formación de las expresiones en lógica de primer orden son las siguientes

Términos

  • una variable es un término
  • una constante es un término
  • si $latex t_1, t_2, \ldots, t_n$ son términos y $latex f$ es una función de aridad $latex n$ > 0, entonces $latex f(t_1, t_2, \ldots, t_n)$ es un término

Fórmulas

  • si $latex P$ es un símbolo de predicado de aridad $latex n \geq 1$ y $latex t_1, t_2, \ldots, t_n$ son términos, entonces $latex P(t_1, t_2, \ldots, t_n)$ es una f.b.f.
  • si $latex \phi$ es una f.b.f., también lo es $latex (\neg \phi)$
  • si $latex \phi$ y $latex \psi$ son f.b.f., también lo son $latex (\phi \land \psi)$,
  • si $latex \phi$ es una f.b.f. y $latex x$ es una variable, entonces $latex (\forall x \phi)$ y $latex (\exists x \phi)$ también son f.b.f.

Una variable $latex x$ que aparece en una fórmula $latex \phi$ es una variable ligada si y sólo si están dentro del ámbito de un cuantificador. En otro caso diremos que es una variable libre.

De la misma forma que la semántica de la lógica proposicional se daba mediante tablas de verdad, en el caso de la lógica de predicados se hace necesario un mecanismo diferente debido a la existencia de las varaibles y la necesidad de realizar sustituciones. De manera que los símbolos de predicado y de función no se pueden evaluar simplemente a verdadero o falso, sino que es necesario disponer de un modelo.

Definición 1. Sea $latex F$ un conjunto de símbolos de función y $latex Pred$ un conjunto de símbolos de predicado. Un modelo $latex M$ del par $latex (F,Pred)$ está formado por

  • un conjunto $latex A$ de valores concretos del universo
  • para cada símbolo de función 0-ario $latex f \in F$, un valor concreto $latex f^M$ de $latex A$. Nota: una función 0-aria es una constante.
  • para cada el resto de símbolos de función $latex f \in F$, una función concreta $latex f^M:A^n \to A$
  • para cada símbolo de predicado $latex P \in Pred$ un subconjunto $latex P^M \subseteq A^n$ de n-tuplas de $latex A$.

De esta forma podemos calcular el valor de verdad de cualquier f.b.f. compuesta por símbolos de función y de predicado, pero todavía no podemos analizar qué ocurre cuando aparecen variables cuantificadas, que nos obligan a interpretar fórmulas de forma relativa a un entorno. Lo haremos mediante tablas de búsqueda $latex l$ que asocian a cada variable $latex x$  un valor $latex l(x)$ del modelo

Definición 2. Una tabla de búsqueda o un entorno para un universo $latex A$ de valores concretos es una función $latex l:var \to A$ definido del conjunto de variables var sobre $latex A$. Denotamos con $latex l[x \mapsto a]$ la tabla que mapea $latex x$ en $latex a$.

Con todo esto ya se puede dar una semántica a la lógica de primer orden. Dado un modelo $latex M$ para un par $latex (F,Pred)$ y dado un entorno $latex l$, se define la satisfacibilidad $latex M \models_l \phi$ para cada f.b.f. $latex \phi$ y entorno $latex l$.

  • $latex M \models_l P(t_1,t_2,\ldots,t_n):$ sii $latex P(a_1,a_2,\ldots,a_n) \in P^M$, donde los términos $latex t_1,t_2,\ldots,t_n$  se interpretan sobre $latex A$ reemplazando todas las variables por sus valores de acuerdo con el entorno $latex l$.
  • $latex M \models_l \forall x \phi:$sii $latex M \models_{l [x\mapsto a]} \phi$ se cumple para todo $latex a \in A$
  • $latex M \models_l \exists x \phi:$ sii $latex M \models_{l [x\mapsto a]} \phi$ se cumple para algún $latex a \in A$
  • $latex M \models_l \neg \phi:$ sii no se da el caso de que se cumpla $latex M \models_l \phi$.
  • $latex M \models_l \phi_1 \land \phi_2:$ sii se cumple  $latex M \models_l \phi_1$ y se cumple  $latex M \models_l \phi_2$.
  • $latex M \models_l \phi_1 \lor \phi_2:$ sii se cumple  $latex M \models_l \phi_1$ o se cumple  $latex M \models_l \phi_2$.
  • $latex M \models_l \phi_1 \to \phi_2:$ sii $latex M \models_l \phi_2$ se cumple siempre que se cumpla  $latex M \models_l \phi_1$.

El problema que aparece en la lógica de primer orden es que no se puede comprobar mecánicamente que $latex \phi_1, \phi_2, \ldots, \phi_n \models \psi$ en el caso general (sí que puede hacerse cuando los predicados son sólo unarios). Por eso se dice que la lógica proposicional es indecidible., porque no hay un algoritmo que tome come entrada una f.b.f. $latex \phi$  y termine siempre con una respuesta correcta que sea verdadero si la f.b.f. es correcta (se evalua a cierto) o falso en caso contrario.

Este mismo problema de indecidibilidad es el que tienen RDF y OWL-Full: no se puede garantizar que un proceso de razonamiento que trata de determinar la veracidad de una fórmula termine en todos los casos. Por eso se emplea habitualmente OWL-DL para razonar en la web semántica y porque la prefiero personalmente: porque es una lógica decidible y suple la pérdida de expresividad (que yo no he notado hasta ahora) con algoritmos de razonamiento que garanbtizan su terminación.

Lógica proposicional

Lógicas y métodos formales 1 Comment »

Empecemos por el principio. La lógica proposicional es la más sencilla. El lenguaje está basado en proposiciones o enunciados declarativos que  son enunciados que pueden evaluarse como ciertos o falsos. Normalmente, se emplean símbolos distintos p, q, r,... para cada enunciado y a partir de ellos se pueden generar expresiones más complejas con operadores lógicos de la forma habitual, usando $latex \land, \lor, \neg, \to$. Por ejemplo, $latex (p \land q) \to (\neg r \lor q)$. Una fórmula bien formada (f.b.f.) se construye empleando exclusivamente las reglas siguientes:

  • cualquier átomo $latex p, q, r, \ldots$ es una f.b.f.
  • si $latex \phi$ es una f.b.f., también lo es $latex (\neg\phi)$
  • si $latex \phi, \psi$ son f.b.f., también lo es $latex (\phi \land \psi )$
  • si $latex \phi, \psi$ son f.b.f., también lo es $latex (\phi \lor \psi )$
  • si $latex \phi, \psi$ son f.b.f., también lo es $latex (\phi \to \psi )$

Otra forma de indicar estas reglas de construcción es usar una gramática BNF, de la forma

$latex \phi ::= p \mid (\neg \phi) \mid (\phi \land \phi) \mid (\phi \lor \phi)\mid (\phi \to \phi)$

La semántica de las expresiones anteriores viene dada por la tabla de verdad correspondiente, que examina el valor de verdad de la expresión $latex \phi$ a partir de todas las combinaciones posibles de los valores de verdad de las proposiciones atómicas. Por ejemplo, para la expresión anterior  $latex (p \land q) \to (\neg r \lor q)$, la tabla de verdad equivalente sería [table id=1 /]

Las reglas de deducción nos permiten construir sistemas de argumentación basados en la lógica, de modo que podemos llegar a una conclusión $latex \psi$ (podemos deducir $latex \psi$) a partir de una serie de proposiones $latex \phi_1, \phi_2,\ldots,\phi_n $. Lo representaremos como 

$latex \phi_1, \phi_2,\ldots,\phi_n \vdash \psi$

Por otro lado, si además para todas las valuaciones en las que las proposiciones $latex \phi_1, \phi_2,\ldots,\phi_n $ se evalúan a T, $latex \psi$ también se evalúa a T, entonces se cumple 

$latex \phi_1, \phi_2,\ldots,\phi_n \models \psi$

donde $latex \models $ es la relación de equivalencia semántica. A partir de estos dos conceptos, deducción y equivalencia semántica, puede estudiarse la corrección (soundness) y la completitud (completeness) de la lógica proposicional. Suelen definirse a partir de estos teoremas

Teorema 1 (corrección). Sean $latex \phi_1, \phi_2,\ldots,\phi_n$ y $latex \psi $ fórmulas proposicionales. Si $latex \phi_1, \phi_2,\ldots,\phi_n \vdash \psi$ es válido entonces se cumple $latex \phi_1, \phi_2,\ldots,\phi_n \models \psi$.

Básicamente, el Teorema 1 quiere decir que todo aquello que se puede deducir a partir de las proposiciones utilizando las reglas de inferencia mantiene el valor de verdad de las proposiciones. O dicho de otra manera, todo lo que se puede deducir es cierto.

Teorema 2 (completitud). Sean $latex \phi_1, \phi_2,\ldots,\phi_n$ y $latex \psi $ fórmulas proposicionales. Si se cumple $latex \phi_1, \phi_2,\ldots,\phi_n \models \psi$ entonces existe una prueba que permite deducir $latex \phi_1, \phi_2,\ldots,\phi_n \vdash \psi$.

De la misma forma, el Teorema 2 quiere decir que si dos expresiones tienen el mismo valor de verdad, podríamos encontrar una argumentación que nos permita deducir una de la otra. O dicho de otra forma, todo lo que es cierto puede deducirse.

WP Theme & Icons by N.Design Studio | Modified by M. Rebollo
RSS Entradas Acceder
Blog logo: MC MECHANIC-HAND FIXING HAND Homage to MC Escher. (c) Shane Willis