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)
∀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.
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.
Clausulas
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
Siendo cada Cj una clausula.
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)}}
