Download Índice 1. Formas normales en lógica de proposiciones

Lógica
1.
Formas normales en lógica de proposiciones
Gracias a las leyes asociativas los paréntesis en (F ∨ (G ∨ H)) o en ((F ∨
G) ∨ H) pueden eliminarse, es decir, se puede escribir (F ∨ G ∨ H). En general
se va a poder escribir sin ambigüedad una fórmula D = (F1 ∨ F2 ∨ . . . ∨ Fn )
donde F1 , F2 , . . . , Fn son fórmulas. La fórmula D es cierta cuando lo es al menos
una de las Fi , en caso contrario D es falsa. La fórmula D recibe el nombre de
disyunción de las fórmulas F1 , F2 , . . . , Fn . De modo análogo se puede escribir
C = (F1 ∧ F2 ∧ ... ∧ Fn ) que es cierta cuando lo son F1 , F2 , . . . , Fn , si alguna de
las Fi es falsa también lo es C. La fórmula C se llama conjunción de F1 , F2 , . . . ,
Fn . El orden en que aparecen los Fi es indiferente debido a la ley conmutativa.
F ORMAS N ORMALES
César Ignacio García Osorio
Índice
1. Formas normales en lógica de proposiciones
1.1. Definiciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2. Método de transformación . . . . . . . . . . . . . . . . . . . . .
2
2
3
1.1. Definiciones
2. Formas normales en lógica de predicados
2.1. Forma normal de prenexa . . . . . . . . . . . . . . . . . . . . . .
2.1.1. Método de transformación . . . . . . . . . . . . . . . . .
2.2. Forma normal de Skolem . . . . . . . . . . . . . . . . . . . . . .
5
5
5
7
Definición 1 (Literal, literales complementarios, par complementario) Un literal es un átomo o la negación de un átomo. Si P , Q, R son átomos P , ¬P ,
Q, ¬Q, R, ¬R son literales. Dos literales l y l son complementarios si y sólo si
l = ¬l . Al conjunto {l, ¬l } se llama par complementario.
Resumen
A menudo es necesario transformar una fórmula en otra, sobre todo
transformar una fórmula a su “forma normal”. Esto se consigue transformando la fórmula en otra equivalente y repitiendo el proceso hasta conseguir
la forma deseada.
En estos apuntes se dan las reglas necesarias para transformar sintácticamente una fórmula en una forma normal más adecuada para la demostración
automática y que conserva la semántica de la fórmula original.
Por ejemplo se pueden usar estas reglas para derivar la fórmula a partir
de otra dada comprobando así la inconsistencia de la fórmula original.
Ahora se pueden definir las formas normales como sigue:
Definición 2 (Forma normal disyuntiva) Una fórmula F se dice que esta en forma normal disyuntiva si y sólo si F es de la forma F = (F1 ∨ F2 ∨ . . . Fn ), donde
cada Fi es una conjunción de literales.
Definición 3 (Forma normal conjuntiva) Una fórmula F se dice que esta en
forma normal conjuntiva si y sólo si F es de la forma F = (F1 ∧ F2 ∧ . . . ∧ Fn ),
donde cada Fi es una disyunción de literales.
Definición 4 (Cláusula, cláusula unitaria, cláusula vacía) Una cláusula es una
disyunción de cero o más literales. A veces se utiliza un conjunto de literales como
equivalente a una cláusula suponiendo la disyunción entre los literales del conjunto. Así por ejemplo P ∨ Q ∨ ¬R = {P, Q, ¬R}. Cuando la cláusula tiene un
único literal se llama cláusula unitaria. Cuando no contiene ningún literal cláusula vacía, como la cláusula vacía no tiene ningún literal no puede ser satisfecha por
ninguna interpretación, la cláusula vacía es siempre falsa y se representa al igual
que la fórmula siempre falsa por .
César I. G. Osorio
2
LSI – Univ. de Burgos
Lógica
1.2
Método de transformación
Definición 5 (Forma clausulada) Una forma clausulada es un conjunto de cláusulas entre las que se supone la conjunción.
Lógica
1.2
Por tanto una forma normal conjuntiva de (P ∧ (Q → R)) → S es (S ∨
¬P ∨ Q) ∧ (S ∨ ¬P ∨ ¬R) la forma clausulada para esta fórmula será:
{{S, ¬P, Q}, {S, ¬P, ¬R}}.
Ejemplo 1
Dados los átomos P , Q y R, la fórmula (¬P ∧ Q) ∨ (P ∧ ¬Q ∧ ¬R) es
una fórmula en forma normal disyuntiva, (P ∨ ¬Q ∨ R) ∧ (¬P ∨ Q) es una
fórmula en forma normal conjuntiva, y {P ∨ ¬Q ∨ R, ¬P ∨ Q} es la forma
clausulada de la fórmula anterior. {{P, ¬Q, R}, {¬P, Q}} es otra forma de
poner la forma clausulada.
Cualquier fórmula se puede transformar en una forma normal. Esta transformación se lleva a cabo mediante la aplicación de las leyes de la El procedimiento
es el siguiente.
1.2.
Método de transformación
Método de transformación
Paso 1: Usar las leyes: (L1) F ↔ G = (F → G) ∧ (G → F ) y (L2) F → G =
¬F ∨ G para eliminar las conectivas lógicas ↔ y →.
Paso 2: Usar repetidamente la ley (L10) ¬(¬F ) = F y las leyes de De Morgan:
(L11.a) ¬(F ∧ H) = ¬F ∨ ¬G y (L11.b) ¬(F ∨ H) = ¬F ∧ ¬G para
disminuir el alcance de la negación a un único literal.
Paso 3: Usar de forma repetida las leyes distributivas: (L5.a) F ∧ (G ∨ H) = (F ∧
G) ∨ (F ∧ H) y (L5.b) F ∨ (G ∧ H) = (F ∨ G) ∧ (F ∨ H) y las otras leyes
para obtener la forma normal.
Ejemplo 2
Obtener la forma normal conjuntiva de la fórmula (P ∧ (Q → R)) → S.
(P
=
=
=
=
=
=
=
=
=
César I. G. Osorio
∧ (Q → R)) → S
(P ∧ (¬Q ∨ R)) → S
¬(P ∧ (¬Q ∨ R)) ∨ S
(¬P ∨ ¬(¬Q ∨ R)) ∨ S
(¬P ∨ (¬(¬Q) ∧ ¬R)) ∨ S
(¬P ∨ (Q ∧ ¬R)) ∨ S
((¬P ∨ Q) ∧ (¬P ∨ ¬R)) ∨ S
S ∨ ((¬P ∨ Q) ∧ (¬P ∨ ¬R))
(S ∨ ((¬P ∨ Q)) ∧ (S ∨ (¬P ∨ ¬R))
(S ∨ ¬P ∨ Q) ∧ (S ∨ ¬P ∨ ¬R)
3
por L2
por L2
por L11.b
por L11.a
por L10
por L6.a
por L3.a
por L6.a
por L4
LSI – Univ. de Burgos
Ejemplo 3
Dadas las fórmulas: F1 = (P → Q), F2 = ¬Q, G = ¬P . Demostrar que G
es consecuencia lógica de F1 y F2 . Esto se podría hacer mediante el uso de
tablas de verdad para comprobar que todo modelo de F1 y de F2 es también
modelo de G. Pero se puede hacer también usando los resultados del teorema
de refutación en combinación con el procedimiento de normalización de
una fórmula. Usando el punto 2 del citado teorema y llevando la fórmula
(((P → Q) ∧ ¬Q) → ¬P ) a forma normal conjuntiva, tenemos:
(((P → Q) ∧ ¬Q) → ¬P )
= ¬((P → Q) ∧ ¬Q) ∨ ¬P
= ¬((¬P ∨ Q) ∧ ¬Q) ∨ ¬P
= ¬((¬P ∧ ¬Q) ∨ (Q ∧ ¬Q)) ∨ ¬P
= ¬((¬P ∧ ¬Q) ∨ ) ∨ ¬P
= ¬((¬P ∧ ¬Q)) ∨ ¬P
= (P ∨ Q) ∨ ¬P
= (Q ∨ P ) ∨ ¬P
= Q ∨ (P ∨ ¬P )
= Q∨
= por L2
por L2
por L5.b
por L8.b
por L6.a
por L11.b
por L3.a
por L4.a
por L8.a
por L7.a
Como la fórmula (((P → Q)∧¬Q) → ¬P ) es válida (ya que es equivalente
a n que es cierta para todo modelo) por el G es consecuencia lógica de F1 y
F2 . Usando el punto 3 del citado teorema de refutación ((P → Q)∧¬Q∧P )
a forma normal disyuntiva, tenemos:
((P → Q) ∧ ¬Q ∧ P )
= (¬P ∨ Q) ∧ ¬Q ∧ P
= (¬P ∧ ¬Q ∧ P ) ∨ (Q ∧ ¬Q ∧ P )
= ∨
= por L2
por L5.b
por L8.b
por L6.a
Como la fórmula ((P → Q) ∧ ¬Q ∧ P ) es inconsistente (ya que es equivalente a que siempre es falsa) por el G es consecuencia lógica de F1 y
F2 . Este último método de probar la inconsistencia de una fórmula transformándola en se llama método de multiplicación, porque el proceso de
César I. G. Osorio
4
LSI – Univ. de Burgos
Lógica
Lógica
transformación es muy similar al de . En el ejemplo anterior se ha mostrado
que la conclusión (G) se sigue de unos hechos dados (F1 y F2 ), llamados
axiomas. La demostración de que la conclusión se sigue de los axiomas se
llama prueba. Un procedimiento para encontrar una prueba se llama procedimiento de prueba. .
2. Formas normales en lógica de predicados
Al igual que en la lógica proposicional en la lógica de predicados también
existen formas normales, un primer paso en la obtención de la forma normal más
adecuada para los procedimientos de deducción automática es llevar todos los
cuantificadores a la parte izquierda de la fórmula: forma normal prenexa, a continuación se transforma la parte de la fórmula sin cuantificadores a la forma normal
conjuntiva de un modo análogo al visto para la lógica de proposiciones, por último se eliminan los cuantificadores universales para obtener la forma normal de
Skolem. Ahora todos los cuantificadores son universales. Podemos representar la
formula como un conjunto de cláusulas siempre y cuando tengamos presente la
mencionada cuantificación universal de las variables.
2.1.
Forma normal de prenexa
Definición 6 (Forma normal prenexa) Una fórmula F de la lógica de predicados se dice que esta en forma normal prenexa si y sólo si la F tiene la forma:
(Q1 x1 )(Q2 x2 ) · · · (Qn xn )M[x1 , x2 , . . . , xn ]
Donde los Qi son cuantificadores: o bien ∃ o bien ∀, y M[x1 , x2 , . . . , xn ] es una
fórmula que no contiene cuantificadores cuyas únicas variables (que son libres)
son x1 , x2 , . . . , xn . (Q1 x1 )(Q2 x2 ) · · · (Qn xn ) se llama prefijo y a M se le llama
matriz de la fórmula F .
2.1.1. Método de transformación
Transformación de una fórmula a su forma normal prenexa.
Paso 1: Usar las leyes
5
Forma normal de prenexa
para eliminar las conectivas lógicas ↔ y →.
Paso 2: Usar repetidamente:
la ley de doble negación
(L10)
¬(¬F ) = F ,
las leyes de De Morgan:
(L11.a) ¬(F ∨ H) = ¬F ∧ ¬G y
(L11.b) ¬(F ∧ H) = ¬F ∨ ¬G,
y las leyes de De Morgan para cuantificadores:
(L13.a) ¬(∀x)F [x] = (∃x)(¬F [x]) y
(L13.b) ¬((∃x)F [x]) = (∀x)(¬F [x])
para llevar los signos de negación inmediatamente delante de los átomos.
Paso 3: Renombrar las variables ligadas si fuese necesario (para poder aplicar las
leyes L15).
Paso 4: Usar las leyes:
(L12.a)
(L12.b)
(L14.a)
(L14.b)
(L15.a)
(L15.b)
G ∨ (Qx)F [x] = (Qx)(G ∨ F [x]),
G ∧ (Qx)F [x] = (Qx)(G ∧ F [x]),
(∀x)F [x] ∧ (∀x)H[x] = (∀x)(F [x] ∧ H[x]),
(∃x)F [x] ∨ (∃x)H[x] = (∃x)(F [x] ∨ H[x]),
(Q1 x)F [x] ∨ (Q2 x)H[x] = (Q1 x)(Q2 z)(F [x] ∨ H[z]) y
(Q3 x)F [x] ∧ (Q4 x)H[x] = (Q3 x)(Q4 z)(F [x] ∧ H[z])
para mover los cuantificadores a la izquierda de la fórmula para obtener la
forma normal prenexa1 .
Ejemplo 4
Obtener la forma normal prenexa de la fórmula: (∀x)(∀y)((∃z)P (x, y, z) ∨
((∃u)Q(x, u) → (∃v)Q(y, v))).
(∀x)(∀y)((∃z)P (x, y, z) ∨ ((∃u)Q(x, u) → (∃v)Q(y, v)))
= (∀x)(∀y)((∃z)P (x, y, z) ∨ (¬(∃u)Q(x, u) ∨ (∃v)Q(y, v)))
= (∀x)(∀y)((∃z)P (x, y, z) ∨ ((∀u)¬Q(x, u) ∨ (∃v)Q(y, v)))
= (∀x)(∀y)(∃z)(∀u)(∃v)(P (x, y, z) ∨ ¬Q(x, u) ∨ Q(y, v))
por L2
por L13.b
usando L12
1
En este último paso es conveniente cuando que los cuantificadores existenciales queden lo más
a la izquierda posible. Los motivos de esto se verán en el capítulo siguiente (cuando se introduzca
el concepto de funciones de Skolem).
(L1) F ↔ G = (F → G) ∧ (G → F ) y
(L2) F → G = ¬F ∨ G
César I. G. Osorio
2.1
LSI – Univ. de Burgos
César I. G. Osorio
6
LSI – Univ. de Burgos
Lógica
2.2
Forma normal de Skolem
La forma normal prenexa es uno de los pasos que hay que seguir para poder transformar una formula en una cláusula, es decir, una formula cerrada de la
forma:
(∀x1 ) · · · (∀xs )(L1 ∨ · · · ∨ Lm )
donde cada Li , i = 1, . . . , m, m ≥ 0, es un literal con Li = Lj para cada i = j, y
x1 , . . . , xs , s ≥ 0, son variables que ocurren en (L1 ∨ · · · ∨ Lm ).
2.2.
Forma normal de Skolem
En el proceso de llevar una fbf a forma clausulada se llega a un punto en el que
hay que eliminar los cuantificadores existenciales. Esto se consigue introduciendo
las llamadas funciones de Skolem. En esta sección se explica la forma de proceder para hacer esto. Además se enuncia y demuestra un importante teorema que
relaciona la insatisfacibilidad de una fbf con la de su forma normal de Skolem.
Sea G una fórmula que ya está en forma normal prenexa
(Q1 x1 )(Q2 x2 ) . . . (Qn xn )M[x1 , x2 , . . . , xn ]
donde M[x1 , x2 , . . . , xn ] está en forma normal conjuntiva. Sea Qr un cuantificador existencial del prefijo (1 ≤ r ≤ n).
Qr se elimina del prefijo y se realizan los siguientes cambios:
(a) Si no hay ningún cuantificador universal delante de Qr
elegir una constate c que no ocurra en M.
reemplazar todas las ocurrencias de xr en M por c.
(b) Sean Qs1 , Qs2 , . . . , Qsm todos los cuantificadores universales que aparecen
delante de Qr con (1 ≤ s1 < s2 . . . sm < r).
elegir una función m-aria fr que no ocurra en M.
reemplazar todas las ocurrencias de xr en M por fr (xs1 , xs1 . . . , xsm ).
Cuando todos los cuantificadores existenciales han sido eliminados por este
procedimiento, la última fórmula obtenida Gs es la forma estándar de Skolem de
G.
Las constantes y funciones utilizadas para reemplazar las variables cuantificadas existencialmente reciben el nombre de funciones de Skolem.
César I. G. Osorio
7
LSI – Univ. de Burgos
Lógica
2.2
Forma normal de Skolem
Ejemplo 5
Obtener la forma estándar de Skolem de la fórmula:
(∃x)(∀y)(∀z)(∃u)(∀v)(∃w)P (x, y, z, u, v, w)
Como ya está en forma normal prenexa y la matriz en forma normal conjuntiva, simplemente tenemos que hacer las eliminaciones de cuantificadores
existenciales. Como (∃x) no está precedido de ningún cuantificador universal, la variable x se sustituye por una constante, por ejemplo a. Como (∃u)
esta precedido por los cuantificadores universales sobre las variables y y z
la variable u se sustituye por la función f (y, z). Por último como (∃w) está precedido por los cuantificadores universales sobre las variables y, z y v
se sustituirá por una función, como por ejemplo g(y, z, v). Con lo cual se
obtiene:
(∀y)(∀z)(∀v)P (a, y, z, f (y, z), v, g(y, z, v))
Ya se había introducido el concepto de cláusula como una disyunción de cero
o más literales, también se ha visto que una cláusula podía representarse como un
conjunto de literales entre los que se supone la disyunción. Del mismo modo un
conjunto de cláusulas S se puede ver como la conjunción de todas las cláusulas
en S, donde cada variable en S se considera que está gobernada por un cuantificador universal. Como ya se ha dicho los cuantificadores existenciales pueden ser
eliminados sin afectar a la propiedad de inconsistencia. Esto es lo que nos dice el
siguiente teorema.
Teorema 1 Sea G una sentencia y Gs su forma estándar de Skolem. G es inconsistente si y sólo si Gs es inconsistente.
Demostración: Sin perdida de generalidad se puede suponer que G está
en forma normal prenexa, es decir:
G = (Q1 x1 )(Q2 x2 ) . . . (Qn xn )M [x1 , x2 , . . . , xn ]
Sea Qr el primer cuantificador existencial de G y G1 igual a:
G1 = (∀x1 ) . . . (∀xr−1 )(Qr+1 xr+1 ) . . . (Qn xn )
M [x1 , . . . , xr−1 , f (x1 , . . . , xr−1 ), xr+1 , . . . , xn ]
con f la función de Skolem correspondiente a xr .
Se va a demostrar que G es inconsistente si y sólo si G1 es inconsistente.
El razonamiento será por reducción al absurdo.
César I. G. Osorio
8
LSI – Univ. de Burgos
Lógica
2.2
Forma normal de Skolem
G inconsistente ⇒ G1 inconsistente.
Sea G inconsistente y supongamos G1 consistente. Por ser G1 consistente existe una interpretación I tal que bajo esa interpretación G1 es
cierta. Es decir para todo x1 , . . . , xr−1 existe al menos un elemento
del dominio, dr = f (x1 , . . . , xr−1 ), tal que la sentencia:
(Qr+1 xr+1 ) . . . (Qn xn )M [x1 , . . . , xr−1 , dr , xr+1 , . . . , xn ]
Lógica
REFERENCIAS
Sea Gs la forma estándar de Skolem de una fórmula G. Si G es inconsistente,
entonces por el teorema 1 G ≡ Gs . Si G no es inconsistente, hay que hacer notar
que en general G no es equivalente a Gs .
Ejemplo 6
Sea G = (∃x)P (x) y Gs = P (a). Claramente Gs es la forma estándar de
Skolem de G. Sin embargo, para la interpretación I definida como:
Dominio:
es cierta en I. Es decir la sentencia:
D = {1, 2}
(Qr+1 xr+1 ) . . . (Qn xn )M [x1 , . . . , xr−1 , xr , xr+1 , . . . , xn ]
Asignación para a:
a
1
es cierta en I para todo x1 , . . . , xr−1 y para algún xr (en concreto existe el xr = dr ). Esto es, G es cierto en I, lo que contradice la asunción
de que G es inconsistente. Por tanto G1 no puede ser consistente.
Asignación para P :
P (1)
F
G1 inconsistente ⇒ G inconsistente.
Sea G1 inconsistente y supongamos G consistente, por ser G consistente existe una interpretación I sobre un dominio D tal que G es
cierta bajo I. Es decir para todo x1 , . . . , xr−1 existe un elemento xr
tal que la sentencia:
(Qr+1 xr+1 ) . . . (Qn xn )M [x1 , . . . , xr−1 , xr , xr+1 , . . . , xn ]
es cierta en I. Extendamos la interpretación I con una función f de
aridad (r−1) que vaya de (x1 , . . . , xr−1 ) en xr para todo x1 , . . . , xr−1
en D, es decir f (x1 , . . . , xr−1 ) = xr . Llamaremos I a esta nueva
interpretación. Con esta definición está claro que la sentencia:
(Qr+1 xr+1 ) . . . (Qn xn )M [x1 , . . . , xr−1 , f (x1 , . . . , xr−1 ), xr+1 , . . . , xn ]
es cierta en I para todo x1 , . . . , xr−1 . Pero esto contradice la asunción
de que G1 fuera inconsistente. Por tanto G debe ser inconsistente.
La demostración del teorema ya es inmediata, por inducción sobre el número
total de cuantificadores existenciales. Si m es el número total de cuantificadores existenciales, hacemos G0 = G y Gk será la fórmula obtenida a partir
de Gk−1 reemplazando el primer cuantificador existencial por una función
de Skolem para k = 1, 2, . . . , m. Claramente Gs = Gm . La demostración
por inducción sobre Gi utiliza los mismos argumentos que el paso de G a
G1 . Por tanto se concluye que G es inconsistente si y sólo si Gs es inconsistente.
César I. G. Osorio
9
LSI – Univ. de Burgos
P (2)
T
claramente, G es cierta en I, pero Gs en falsa en I. Por tanto G = Gs .
Es evidente que una fórmula puede tener más de una forma normal de Skolem,
por simplicidad cuando se transforma una fórmula G en su forma estándar Gs es
conveniente reemplazar los cuantificadores existenciales por funciones de Skolem
que sean lo más simples posibles, esto significa que tengan el menor número de
variables posibles. Cuando se tiene una fórmula como F = F1 ∧ . . . ∧ Fn , se
puede obtener el conjunto de cláusulas S que representa la forma estándar de
Skolem de F hallando los conjuntos de cláusulas Si que representan las formas
normales de Skolem de cada Fi y calculando la unión de los mismos. Se tiene que
S = S1 ∪ . . . ∪ Sn . Usando argumentos similares a los dados en el teorema 1 no
es difícil ver que F es inconsistente si y sólo si S es inconsistente.
Referencias
[CCT73]
Chin-Liang Chang y Lee Richard Char-Tung. Symbolic Logic and
Mechanical Theorem Proving. Computer science classics. Academic
Press, 1973.
[LVDG91] Peter Lucas y Linda Van Der Gaag. Principles of expert systems.
Addison-Wesley, 1991.
César I. G. Osorio
10
LSI – Univ. de Burgos