Dentro de la logica predictiva encontramos diferentes formulas expresadas mediante los cuantores universales y existencias asi como logicos. Sabemos que cualquier formula de lenguaje de enunciados puede reducirse a su forma normal conjuntiva(una conjuncion de disyunciones elementales o una disyuncion elemental). Estas disyunciones elementales son llamadas clausulas y la formula atomica o su negacion es llamada literal.
Una clausula es una disyunción finita L1 V L2 V … V Ln de literales, donde L1 ≠ L2 ≠… Ln
Una clausula es positiva si consta solo de literales positivos, y negativa si todos sus literales son negativos. En la clausula positiva, al menos uno de los literales es verdadero.
En algunas ocasiones resulta conveniente hablar también de una "clausula vacía" que aparece en la inferencia cuando las premisas son incompatibles.
¿Qúe podemos hacer cuando queremos demostrar un hecho a partir de un conjunto de formulas con cuantificadores existenciales?
La respuesta está en transformar una fórmula con varios cuantificadores a una que solo tenga cuantificadores universales. Esto se puede hacer mediante skolemización.
La skolemización(por Toraf Skolem) tiene por objeto transformar una fórmula a otra equivalente en forma normal prenex.
¿Qué es la forma normal prenex(prenexa)?
Una fórmula prenex solo tiene cuantificadores al comienzo de ésta. Por ejemplo:
∀xy∃ z (P(x,
y) à R(x, y, z)) es una fórmula
prenex.
Una fórmula F
de un lenguaje de primer orden está a en forma normal prenexa (o forma prenex)
si es de la forma
Q1 x1 Q2 x2
Qn xn G(x1; … ; xn)
Donde Qi ϵ {∃
∀} es
abierta y G(x1;…; xn) es abierta Es decir, una formula en forma prenex esta
formada por un bloque inicial de cuanticadores seguido por una formula abierta.
Una fórmula
prenex solo tiene cuantificadores al
comienzo de ésta. Por ejemplo:
∀xy∃ z (P(x, y) à R(x, y, z)) es una
fórmula prenex.
Objetivo:
Restringir la complejidad sintáctica de las formulas de primer orden, sin
perder expresividad. Trabajaremos con fórmulas cerradas.
- Primer paso: Trasladar los cuanticadores a la izquierda obteniendo un forma normal prenexa.
- El siguiente paso es eliminar los cuanticadores existenciales hasta obtener una f fórmula universal (es decir, una fórmula en forma prenex que s solo contiene cuanticadores universales).
- La fórmula universal obtenida al de estas transformaciones es una forma de Skolem de la fórmula inicial.
- El proceso de eliminación aumenta el lenguaje con nuevos símbolos de función y nuevas constantes.
- En general, NO existe equivalencia entre la fórmula obtenida y la fórmula inicial, aunque se conserva la consistencia de la formula original.
Funciones y constantes
de Skolem
Para eliminar los cuanticadores existenciales
de una formula en forma prenexa aplicamos las siguientes reglas:
Por cada bloque
∀x1… ∀xn ∃y (x1;…; xn; y)
- Introducir un nuevo símbolo de función g (aridad n), y rescribir como
∀x1 … ∀xnF(x1; …; xn; g(x1; …; xn))
(Decimos que ∀x1… ∀xn F(x1;…; xn; g(x1;…; xn))
se obtiene a partir de
∀x1…∀xn∃yF (x1; xn; y)
introduciendo una función de Skolem).
- Por cada bloque del tipo ∃xF (x) añadir una nueva constante c y rescribir como F(c). (Se dice que F(c) se obtiene a partir de ∃x F(x) introduciendo una constante de Skolem).
- G se denomina una función de Skolem y c una constante de Skolem.
- La introducción de funciones y constantes de Skolem conserva la consistencia. Es decir, dada una fórmula F, si F’ se obtiene a partir de F introduciendo una función o una constante de Skolem, entonces,
F tiene un
modelo ↔ F’ tiene
un modelo.
- Además, la introducción de funciones y constantes de Skolem, no aumenta el conocimiento deducible en el lenguaje original.
Es decir,
Si F es una fórmula cerrada de un lenguaje de primer orden L y F’ se
obtiene a partir de F introduciendo una función o una constante de Skolem,
entonces para toda fórmula H del lenguaje L se tiene:
F’ |= H ↔ F |=
H
Ejemplos
∀x∃y∃z (Padre de (y; x) ^ Padre
de (z; y))
+Dependencia de y con respecto a x: Elegimos mediante una función f1:
∀x∃z (Padre de (f1(x); x) ^ Padre de (z; f1(x)))
+ Dependencia de z con respecto a x: Elegimos mediante una función f2:
∀x (Padre de (f1(x); x) ^ Padre de (f2(x); f1(x)))
+ La fórmula universal
∀x (Padre de (f1(x); x) ^ Padre de (f2(x); f1(x)))
es una Forma de Skolem de la fórmula inicial.
Sea L un Lógica de primer orden.
+ Una fórmula F es un literal si es una fórmula atómica o la
negación de una fórmula atómica.
+ Una cláusula es una disyunción de literales. Por tanto, es una fórmula
abierta.
+ Como en el caso de la lógica proposicional, identificaremos una clausula
con el conjunto de los literales que aparecen en ella.
+ Denotaremos por □ a la
clausula vacía.
+ Dada una formula F de L una forma clausal de F es un conjunto de
clausulas S (no necesariamente del lenguaje L) tal que
F tiene un
modelo ↔ S tiene un modelo
Forma clausal
Para obtener una forma clausal de una fórmula
F(x1;…; xn) seguimos los siguientes pasos:
1. Obtener el
cierre universal de F(x1;…; xn). Es decir, la fórmula G dada por ∀x1…∀xn F(x1;…; xn).
2. Obtener una
forma de Skolem de G. Dicha forma de Skolem es una fórmula universal G(S) .
3. Eliminar
los cuantificadores universales de G(S). Así obtenemos una formula abierta H.
4. Obtener una
forma normal conjuntiva de H (siguiendo el mismo procedimiento que en el caso
proposicional). Dicha forma será:
n
^ Cj
j=1
5. La forma clausal de F es
el conjunto de clausulas
S = {C1;…; Cn
Ejemplo
+Forma
clausal:
{{¬Hermano(x, F1(x)), u = F2(x), Padre de (F2(x),
u)}}
∀x∀z(x < z -->∃y(x < y ^ y < z))
+Forma clausal
((¬(x < z) ˅ x < f (x, z)) ^ (¬(x < z)
˅ f (x, z) < z))
+ O también
{{¬(x < z), x < f (x, z)}, {¬(x < z),
f (x; z) < z)}}
Se puso muy formal el asunto, mientras la meta era algo más aplicado. Te pongo 9 pts.
ResponderEliminar