PDF de programación - Tema 2: Formas normales

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Tema 2:

Formas normales

Dpto. Ciencias de la Computación Inteligencia Artificial

Universidad de Sevilla

Lógica Informática

(Tecnologías Informáticas)

Curso 2015–16

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Contenido

Equivalencia lógica

Sustitución

Formas normales

Forma clausal

Algoritmos para SAT y TAUT

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Introducción

En este tema estudiaremos una visión algebraica de las

fórmulas proposicionales.

Si identificamos cada conectiva con su función de

verdad, entonces cada fórmula proposicional F , que
contenga sólo las variables proposicionales p1, . . . , pn,
puede considerarse una expresión algebraica (similar a
un polinomio), que define una función booleana
HF : {0, 1}n → {0, 1}.

Estas expresiones algebraicas pueden manipularse de

manera similar al modo en que reescribimos una
expresión aritmética para simplificarla. Conseguiremos
así dos formas simples para cada fórmula: la forma
normal conjuntiva y la forma normal disyuntiva.

Equivalencia lógica
Dos fórmulas F1, F2 son equivalentes (F1 ≡ F2) si, para
toda valoración v , v (F1) = v (F2). Es decir, F1 ≡ F2 si F1 y
F2 tienen los mismos modelos.

F1 ≡ F2 si y sólo si F1 |= F2 y F2 |= F1

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Ejemplos:

Cualesquiera dos fórmulas insatisfactibles son

equivalentes.

Dos tautologías cualesquiera son equivalentes.
. . .

Equivalencias (I)
Sean A, B ∈ PROP. Se tienen las siguientes equivalencias:
Conmutatividad: A ∨ B ≡ B ∨ A y A ∧ B ≡ B ∧ A
Asociatividad:

A∨(B∨C ) ≡ (A∨B)∨C

y A∧(B∧C ) ≡ (A∧B)∧C

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Distributividad:

A ∧ (B ∨ C ) ≡ (A ∧ B) ∨ (A ∧ C )
A ∨ (B ∧ C ) ≡ (A ∨ B) ∧ (A ∨ C )

Doble negación: ¬¬A ≡ A
Leyes de De Morgan:
¬(A ∧ B) ≡ ¬A ∨ ¬B

y ¬(A ∨ B) ≡ ¬A ∧ ¬B

Equivalencias (II)

Idempotencia: A ∨ A ≡ A y A ∧ A ≡ A
Absorción: A ∨ (A ∧ B) ≡ A y A ∧ (A ∨ B) ≡ A
Leyes de tautología: Si A es una tautología, entonces

A ∧ B ≡ B

y

A ∨ B ≡ A

Leyes de inconsistentes: Si A es insatisfactible,

entonces

A ∧ B ≡ A

y

A ∨ B ≡ B

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Sustitución

Dadas A, B ∈ PROP si A es una subfórmula de B y

A ∈ PROP, la sustitución de A por A en B es la
fórmula que se obtiene al cambiar cada aparición de A
en B por A.

Notación: B{A/A}.
Si A no es una subfórmula de B, por definición

Ejemplo: Si B es p → (q ∧ r ) ∨ ¬s, A es q ∧ r y A es

B{A/A} es B.

t → ¬r , entonces



∨¬s

B



A

p → (q ∧ r )



B{A/A}
p → (t → ¬r )



A



∨¬s



Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Sustitución: ejemplos
Si B es p → q → r ∨ s entonces:

B{r ∨ s/p} es

B{q ∧ r /q} es

B{q → r ∨ s/p ∧ r} es

p → q → p.

p → q → r ∨ s.

p → p ∧ r .

p → q → r ∨ s.

B{p → q/p} es

Si C es la fórmula (p → q) ∨ (r → p → q), entonces

C{p → q/t} es
C{p → q/t → p → q} es

t ∨ (r → t).

(t → p → q) ∨ (r → (t → p → q)).

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

El Teorema de sustitución
Teorema de Sustitución. Sean B ∈ PROP y
A, A ∈ PROP tales que A ≡ A. Entonces

B{A/A} ≡ B

El teorema de sustitución nos permite manipular

“algebraicamente” una fórmula F para obtener otra
fórmula más simple y equivalente a F . Este proceso es
similar al empleado en la simplificación de expresiones
algebraicas.

Ejemplo:

B ∨ (A ∧ (A → B)) ≡ B ∨ (A ∧ (¬A ∨ B))

≡ B ∨ (A ∧ ¬A) ∨ (A ∧ B)
≡ B ∨ (A ∧ B) ≡ B

Literales

Una fórmula F es un literal si es una variable

proposicional o la negación de una variable
proposicional.

Dos literales, L1 y L2, son complementarios (se dice
que uno es el complementario del otro) si uno de ellos
es la negación del otro.

Lema 1. Sean L1, . . . , Ln literales. Son equivalentes:

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

n

n

Li es una tautología.

1.
2. {L1, . . . , Ln} contiene un par de literales

i=1

complementarios.

Lema 2. Sean L1, . . . , Ln literales. Son equivalentes:

Li es insatisfactible

1.
2. {L1, . . . , Ln} contiene un par de literales

i=1

complementarios.

Formas normales

Una fórmula está en Forma normal conjuntiva (FNC)

si es una conjunción de disyunciones de literales:

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

F =

Li,j

n

i=1

n

j=1

 mi
 mi




Una fórmula está en Forma normal disjuntiva (FND)

si es una disyunción de conjunciones de literales:

F =

Li,j

i=1

j=1

Formas normales (II)

Lema:

Una fórmula en forma normal conjuntiva es una

tautología syss cada una de sus disyunciones es una
tautología.

Una fórmula en forma normal disjuntiva es

insatisfactible syss cada una de sus conjunciones es
insatisfactible.

Teorema.

Para toda fórmula G existe F en FNC tal que F ≡ G .
Para toda fórmula G existe F en FND tal que F ≡ G .

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Paso a forma normal

Procedimiento para transformar G en FNC:

1. Eliminar todas las implicaciones usando:

A → B ≡ ¬A ∨ B

y A ↔ B ≡ (A → B) ∧ (B → A)

2. Trasladar las negaciones, mediante las leyes de Morgan:
¬(A ∨ B) ≡ ¬A ∧ ¬B

¬(A ∧ B) ≡ ¬A ∨ ¬B

y

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

3. Eliminar negaciones dobles usando ¬¬A ≡ A.
4. Convertir a FNC utilizando la ley distributiva:
A ∨ (B1 ∧ B2) ≡ (A ∨ B1) ∧ (A ∨ B2)

Para pasar a FND utilizamos la ley distributiva:
A ∧ (B1 ∨ B2) ≡ (A ∧ B1) ∨ (A ∧ B2)

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Ejemplo:
Para obtener una FNC de (¬p ∧ q) → (q ∨ r ) → p siguiendo
el procedimiento anterior:

(¬p ∧ q) → (q ∨ r ) → p

⇒

⇒
⇒
⇒
⇒
⇒
⇒

¬(¬p ∧ q) ∨ ((q ∨ r ) → p)
¬(¬p ∧ q) ∨ ¬(q ∨ r ) ∨ p
¬¬p ∨ ¬q ∨ (¬q ∧ ¬r ) ∨ p
p ∨ ¬q ∨ ((¬q ∨ p) ∧ (¬r ∨ p))
(p ∨ ¬q ∨ ¬q ∨ p) ∧ (p ∨ ¬q ∨ ¬r ∨ p)
(¬q ∨ p) ∧ (¬q ∨ ¬r ∨ p)

Hemos eliminado literales repetidos en una misma cláusula
gracias a la equivalencia: A ∨ A ≡ A.
(En la FND utilizaríamos la equivalencia A ∧ A ≡ A).

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Cláusulas

Una cláusula es una disyunción de literales

L1 ∨ ··· ∨ Ln.

Dada una valoración v y una cláusula L1 ∨ ··· ∨ Ln:

v |= L1∨···∨Ln ⇐⇒ Existe i = 1, . . . , n tal que v |= Li
Por tanto, el valor de verdad de L1 ∨ ··· ∨ Ln no
depende ni del orden en que aparecen los literales ni de
posibles repeticiones de literales.

En consecuencia, identificamos la cláusula L1 ∨ ··· ∨ Ln

con el conjunto de literales {L1, . . . Ln}.

Caso especial: la cláusula vacía, correspondiente al

conjunto de literales vacío. La denotamos por .
Por definición, para toda valoración, v , se tiene

v () = 0.

Notación: Lc denota al literal complementario de L.

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

Formas clausales

Para toda fórmula F ∈ PROP existe un conjunto de

cláusulas {C1, . . . , Cn} tal que para toda valoración, v ,

v |= F ⇐⇒ v |= {C1, . . . , Cn}

{C1, . . . , Cn} se denomina una forma clausal de F .
Podemos obtener una forma clausal a partir de una

forma normal conjuntiva.

La fórmula en forma normal conjuntiva

(L1,1 ∨ ··· ∨ L1,n1) ∧ ··· ∧ (Lm,1 ∨ ··· ∨ Lm,nm)

se escribe en forma clausal:

{{L1,1, . . . , L1,n1} . . .{Lm,1,··· , Lm,nm}}

Formas clausales (II)

En el caso de un conjunto de fórmulas U existe un

conjunto de cláusulas {C1, . . . , Cn} tal que para toda
valoración, v ,

v |= U ⇐⇒ v |= {C1, . . . , Cn}

{C1, . . . , Cn} se denomina una forma clausal del
conjunto U.

Podemos obtener una forma clausal de un conjunto U

Formas normales

Equivalencia lógica
Sustitución

Formas normales

Forma clausal

Algoritmos para
SAT y TAUT

uniendo formas clausales de las fórmulas de U.

Ejemplo:

U = {p → q

, (p ∨ ¬q) ∧ (r → ¬p)

(1)



{¬p ∨ q

(1)



(2)



(2)

Una forma clausal de U es:

, p ∨ ¬q, ¬r ∨ ¬p

, p, ¬r



}

(3)

, p ∧ ¬r



}

(3)

Algoritmo de satisfactibilidad mediante FND

Formas normales

Entrada: Una fórmula F .
Salida: Satisfactible, si F es satisfactible;
Insatisfactible, en caso contrario.

Procedimiento
Calcular una FND de F , FND(F