LIT4: Formales normales conjuntivas y disyuntivas

Se presenta las formas normales conjuntivas y disyuntivas como medio para resolver los problemas TAUT y SAT.

Este es el tema 4 del curso de "Lógica informática". Más temas en http://www.cs.us.es/~jalonso/cursos/li/temas.html

1. PD Tema 4: Formas normales
Lógica informática (201314)
Tema 4: Formas normales
José A. Alonso Jiménez
Andrés Cordón Franco
María J. Hidalgo Doblado
Grupo de Lógica Computacional
Departamento de Ciencias de la Computación e I.A.
Universidad de Sevilla
1 / 20

2. PD Tema 4: Formas normales
Tema 4: Formas normales
1.
2.
3.
2 / 20

3. PD Tema 4: Formas normales
Forma normal conjuntiva
Tema 4: Formas normales
1.
Denición de forma normal conjuntiva
Algoritmo de cálculo de forma normal conjuntiva
Decisión de validez mediante FNC
2.
3.
3 / 20

4. PD Tema 4: Formas normales
Forma normal conjuntiva
Denición de forma normal conjuntiva
Forma normal conjuntiva
IÁtomos y literales:
IDef.: Un p;q; : : :).
IDef.: Un p;:p;q;:q; : : :).
INotación:L;L1;L2; : : :representarán literales.
IForma normal conjuntiva:
IDef.: Una fórmula está enFNC) si es
una conjunción de disyunciones de literales; es decir, es de la forma
(L1;1_ _L1;n1)^ ^(Lm;1_ _Lm;nm).
IEjemplos:(:p_q)^(:q_p)está en FNC.
(:p_q)^(q!p)no está en FNC.
IDef.: Una fórmulaGes unaFNC) de la
fórmulaFsiGestá en forma normal conjuntiva y es equivalente a
F.
IEjemplo: Una FNC de:(p^(q!r))es(:p_q)^(:p_ :r).
4 / 20

5. PD Tema 4: Formas normales
Forma normal conjuntiva
Algoritmo de cálculo de forma normal conjuntiva
Algoritmo de cálculo de forma normal conjuntiva
Algoritmo: Aplicando a una fórmula Flos siguientes pasos se obtiene
una forma normal conjuntiva deF, FNC(F):
1.
A$B(A!B)^(B!A) (1)
2.
A!B :A_B (2)
3.
:(A^B) :A_ :B (3)
:(A_B) :A^ :B (4)
::AA (5)
4.
A_(B^C)(A_B)^(A_C) (6)
(A^B)_C(A_C)^(B_C) (7)
5 / 20

6. PD Tema 4: Formas normales
Forma normal conjuntiva
Algoritmo de cálculo de forma normal conjuntiva
Ejemplos de cálculo de forma normal conjuntiva
IEjemplo de cálculo de una FNC de:(p^(q!r)):
:(p^(q!r))
(p^(:q_r)) [por (2)]
:p_(:q_r) [por (3)]
:p_(::q^ :r) [por (4)]
p_(q^ :r) [por (5)]
(:p_q)^(:p_ :r)[por (6)]
IEjemplo de cálculo de una FNC de(p!q)_(q!p):
(p!q)_(q!p)
(:p_q)_(:q_p)[por (2)]
:p_q_ :q_p
6 / 20

7. PD Tema 4: Formas normales
Forma normal conjuntiva
Algoritmo de cálculo de forma normal conjuntiva
Cálculo de forma normal conjuntiva
IEjemplo de cálculo de una FNC de(p$q)!r:
(p$q)!r
(p!q)^(q!p)!r [(1)]
:((p!q)^(q!p))_r [(2)]
((:p_q)^(:q_p))_r [(2)]
(:(:p_q)_(:q_p))_r [(3)]
((::p^ :q)_(::q^ :p))_r [(4)]
((p^ :q)_(q^ :p))_r [(5)]
(((p^ :q)_q)^((p^ :q)_ :p))_r [(6)]
(((p_q)^(:q_q))^((p_ :p)^(:q_ :p)))_r [(7)]
(((p_q)^(:q_q))_r)^(((p_ :p)^(:q_ :p))_r) [(7)]
(((p_q)_r)^((:q_q)_r))^(((p_ :p)_r)^((:q_ :p)_r))[(7)]
(p_q_r)^(:q_q_r)^(p_ :p_r)^(:q_ :p_r)
(p_q_r)^(:q_ :p_r)
7 / 20

8. PD Tema 4: Formas normales
Forma normal conjuntiva
Decisión de validez mediante FNC
Procedimiento de decisión de validez mediante FNC
ILiterales complementarios:
IEl LesL
c
=

:psiL=p;
p siL=:p.
IPropiedades de reducción de tautologías:
IF1^ ^Fnes una tautología syssF1; : : : ;Fnlo son.
IL1_ _Lnes una tautología syssfL1; : : : ;Lngcontiene algún par
de literales complementarios (i.e. existeni;jtales queLi=L
c
j
).
IAlgoritmo de decisión de tautologías mediante FNC
IEntrada: Una fórmulaF.
IProcedimiento:
1. F.
2.
de literales complementarios.
8 / 20

9. PD Tema 4: Formas normales
Forma normal conjuntiva
Decisión de validez mediante FNC
Ejemplos de decisión de validez mediante FNC
I:(p^(q!r))no es tautología:
FNC(:(p^(q!r))) = (:p_q)^(:p_ :r)
Contramodelos de:(p^(q!r)):
I1tal queI1(p) =1 yI1(q) =0
I2tal queI2(p) =1 yI2(r) =1
I(p!q)_(q!p)es tautología:
FNC((p!q)_(q!p)) =:p_q_ :q_p
I(p$q)!rno es tautología:
FNC((p$q)!r) = (p_q_r)^(:q_ :p_r)
Contramodelos de(p$q)!r:
I1tal queI1(p) =0;I1(q) =0 yI1(r) =0
I2tal queI2(p) =1;I2(q) =1 yI2(r) =0
9 / 20

10. PD Tema 4: Formas normales
Forma normal disyuntiva
Tema 4: Formas normales
1.
2.
Denición de forma normal disyuntiva
Algoritmo de cálculo de forma normal disyuntiva
Decisión de satisfacibilidad mediante FND
3.
10 / 20

11. PD Tema 4: Formas normales
Forma normal disyuntiva
Denición de forma normal disyuntiva
Denición de forma normal disyuntiva
IDef.: Una fórmula está enFND) si es
una disyunción de conjunciones de literales; es decir, es de la
forma
(L1;1^ ^L1;n1
)_ _(Lm;1^ ^Lm;nm).
IEjemplos:(:p^q)_(:q^p)está en FND.
(:p^q)_(q!p)no está en FND.
IDef.: Una fórmulaGes unaFND) de la
fórmulaFsiGestá en forma normal disyuntiva y es equivalente
aF.
IEjemplo: Una FND de:(p^(q!r))es:p_(q^ :r).
11 / 20

12. PD Tema 4: Formas normales
Forma normal disyuntiva
Algoritmo de cálculo de forma normal disyuntiva
Algoritmo de cálculo de forma normal disyuntiva
Algoritmo: Aplicando a una fórmula Flos siguientes pasos se obtiene
una forma normal disyuntiva deF, FND(F):
1.
A$B(A!B)^(B!A) (1)
2.
A!B :A_B (2)
3.
:(A^B) :A_ :B (3)
:(A_B) :A^ :B (4)
::AA (5)
4.
A^(B_C)(A^B)_(A^C) (6)
(A_B)^C(A^C)_(B^C) (7)
12 / 20

13. PD Tema 4: Formas normales
Forma normal disyuntiva
Algoritmo de cálculo de forma normal disyuntiva
Ejemplos de cálculo de forma normal disyuntiva
IEjemplo de cálculo de una FND de:(p^(q!r)):
:(p^(q!r))
(p^(:q_r))[por (2)]
:p_(:q_r)[por (3)]
:p_(::q^ :r)[por (4)]
:p_(q^ :r) [por (5)]
IEjemplo de cálculo de una FND de:(:p_ :q! :(p^q)):
:(:p_ :q! :(p^q))
(:(:p_ :q)_ :(p^q)) [por (2)]
(:p_ :q)^ (p^q) [por (4)]
(:p_ :q)^(p^q) [por (5)]
(:p^(p^q))_(:q^(p^q))[por (7)]
(:p^p^q)_(:q^p^q)
13 / 20

14. PD Tema 4: Formas normales
Forma normal disyuntiva
Decisión de satisfacibilidad mediante FND
Procedimiento de decisión de satisfacibilidad mediante
FND
IPropiedades de reducción de satisfacibilidad:
IF1_ _Fnes satisfacible syss alguna de las fórmulasF1; : : : ;Fn
lo es.
IL1^ ^Lnes satisfacible syssfL1; : : : ;Lngno contiene ningún
par de literales complementarios.
IAlgoritmo de decisión de satisfacibilidad mediante FND:
IEntrada: Una fórmulaF.
IProcedimiento:
1. F.
2.
de literales complementarios.
14 / 20

15. PD Tema 4: Formas normales
Forma normal disyuntiva
Decisión de satisfacibilidad mediante FND
Ejemplos de decisión de satisfacibilidad mediante FND
I:(p^(q!r))es satisfacible:
FND(:(p^(q!r))) =:p_(q^ :r)
Modelos de:(p^(q!r)):
I1tal queI1(p) =0
I2tal queI2(q) =1 yI2(r) =0
I:(:p_ :q! :(p^q))es insatisfacible:
FND(:(:p_ :q! :(p^q))) = (:p^p^q)_(:q^p^q)
15 / 20

16. PD Tema 4: Formas normales
Cálculo de formas normales mediante tableros semánticos
Tema 4: Formas normales
1.
2.
3.
Forma normal disyuntiva por tableros
Forma normal conjuntiva por tableros
16 / 20

17. PD Tema 4: Formas normales
Cálculo de formas normales mediante tableros semánticos
Forma normal disyuntiva por tableros
Forma normal disyuntiva por tableros
IProp.: SeaFuna fórmula. Si las hojas abiertas de un tablero
completo defFgsonfL1;1; : : : ;L1;n1
g; : : : ;fLm;1; : : : ;Lm;nmg,
entonces una forma normal disyuntiva deFes
(L1;1^ ^L1;n1
)_ _(Lm;1^ ^Lm;nm).
17 / 20

18. PD Tema 4: Formas normales
Cálculo de formas normales mediante tableros semánticos
Forma normal disyuntiva por tableros
Forma normal disyuntiva por tableros
IEjemplo: Forma normal disyuntiva de:(p_q!p^q).
:(p_q!p^q)p_q;:(p^q)p;:(p^q)p;:p?p;:qq;:(p^q)q;:pq;:q?
Una forma normal disyuntiva de:(p_q!p^q)es
(p^ :q)_(q^ :p).
18 / 20

19. PD Tema 4: Formas normales
Cálculo de formas normales mediante tableros semánticos
Forma normal conjuntiva por tableros
Forma normal conjuntiva por tableros
IProp.: SeaFuna fórmula. Si las hojas abiertas de un tablero
completo def:FgsonfL1;1; : : : ;L1;n1
g; : : : ;fLm;1; : : : ;Lm;nmg,
entonces una forma normal conjuntiva deFes
(L
c
1;1
_ _L
c
1;n1
)^ ^(L
c
m;1
_ _L
c
m;nm
).
IEjemplo: Forma normal conjuntiva dep_q!p^q.
IUn árbol completo:(p_q!p^q)está en la transparencia
anterior.
IUna forma normal disyuntiva de:(p_q!p^q)es
(p^ :q)_(q^ :p).
IUna forma normal conjuntiva dep_q!p^qes
(:p_q)^(:q_p).
p_q!p^q ::(p_q!p^q)
:((p^ :q)_(q^ :p))
:(p^ :q)^ :(q^ :p))
(:p_ ::q)^(:q_ ::p))
(:p_q)^(:q_p))
19 / 20

20. PD Tema 4: Formas normales
Bibliografía
Bibliografía
1. Elementos de lógica formal.
(Ariel, 2000)
Cap. 8 (Equivalencia lógica) y 10 (Formas normales).
2. Mathematical logic for computer science (2nd ed.).
(Springer, 2001)
Cap. 2 (Propositional calculus: formulas, models, tableaux).
3. Iniciación a la Lógica, (Ariel, 2002)
Cap. 3 (Semántica formal. Consecuencia lógica).
4. Logic in computer science: modelling and
reasoning about systems.(Cambridge University Press, 2000)
Cap. 1 (Propositional logic).
5. Lógica computacional
(Thomson, 2003)
Cap. 4.4 (Formas normales).
20 / 20