Forma Normal Disyuntiva - DNF

Verificación y Validación de Software
Agregado 1

Como tarea extra realice un ejemplo pequeño de una proposición y que lo pasaré a la forma normal disyuntiva, que se denota por DNF por sus siglas en inglés.

La idea de esto es inventar cualquier proposición, y mediante leyes de equivalencia, como las leyes de Morgan, hagamos que nuestra proposición quede expresada únicamente con los operadores de negación y disyunción, que se denota así {¬, ∨}.

Entonces la proposición simple que invente es.

(¬c → b)^(c → ¬a)

Y ahora vamos a cambiar los operadores usados para que quede, como ya dije, con operadores de negación y disyunción.

Por si tienen duda de las leyes de equivalencia, yo encontré en la siguiente página las más básicas y que me ayudaron en la realización de esta tarea.

Leyes de equivalencia

Entonces tenemos que:

(¬c → b) ^ (c → ¬a)
Primero pasamos a eliminar los operadores condicionales que están dentro de los paréntesis, con la ley de Implicación Material.

(¬¬c ∨ b) ^ (¬c ∨ ¬a)
Simplificamos la parte del doble operador negativo.

(c ∨ b) ^ (¬c ∨ ¬a)
Luego para eliminar la conjunción, usamos las leyes de Morgan.

¬[¬(c ∨ b) ∨ ¬(¬c ∨ ¬a)]

Y ahora ya tenemos la proposición expresada solo con operadores de negación y de disyunción. Ahora vamos a probar si la original, con esta última nos dan como resultado la misma tabla de verdad.

Para ahorrar tiempo use el mismo programa que había creado para verificar si una proposición era una tautología, y probé estas dos proposiciones.


Entonces para (¬c → b) ^ (c → ¬a) el siguiente resultado.

esteban@presario:~/Documents/programas/verificacion$ ./tabla_de_verdad.py 
conjuncion(condicional(negacion(C),B) , condicional(C,negacion(A)))
a b c  S
0 0 0  0
0 0 1  1
0 1 0  1
0 1 1  1
1 0 0  0
1 0 1  0
1 1 0  1
1 1 1  0

Y para ¬[¬(c ∨ b) ∨ ¬(¬c ∨ ¬a)] se obtuvo.

esteban@presario:~/Documents/programas/verificacion$ ./tabla_de_verdad.py 
negacion(disyuncion(negacion(disyuncion(C,B)),negacion(disyuncion(negacion(C),negacion(A)))))
a b c S
0 0 0  0
0 0 1  1
0 1 0  1
0 1 1  1
1 0 0  0
1 0 1  0
1 1 0  1
1 1 1  0

Y como podemos observar, en las dos tablas de verdad obtenemos los mismos valores en la salida S.

Ahora con mapas de Karnaugh

También es posible obtener la proposición en DNF, mediante códigos de Gray y mapas de Karnaugh.

Para esto partimos de la proposición original (¬c → b) ^ (c → ¬a) y obtenemos sus valores de salida junto con los códigos Gray, en una tabla de verdad.

a b c S
0 0 0  0
0 0 1  1
0 1 0  1
0 1 1  1
1 0 0  0
1 0 1  0
1 1 0  1
1 1 1  0

Y ahora usando mapas de Karnaugh obtendremos la forma normal disyuntiva (DNF).

c \ ab	00	01	11	10
0	0	1	1	0
1	1	1	0	0

Y los mapas nos dan la proposición a'c + bc', que podemos escribir también como (¬a^c) ∨ (b^¬c), y en base a la definición de wikipedia de "una fórmula está en forma normal disyuntiva (DNF) si corresponde a una disyunción de cláusulas conjuntivas" [1], sabemos que lo que esta entre paréntesis son las cláusulas conjuntivas, y hay una disyunción entre los dos.

Con el programa volvemos a probar con esta nueva fórmula, y vemos que la tabla de verdad sigue dando los mismos resultados de salida.

esteban@presario:~/Documents/programas/verificacion$ ./tabla_de_verdad.py 
disyuncion(conjuncion(negacion(A),C),conjuncion(B,negacion(C)))
a b c S
0 0 0  0
0 0 1  1
0 1 0  1
0 1 1  1
1 0 0  0
1 0 1  0
1 1 0  1
1 1 1  0

Recursos consultados:
[1] Forma normal disyuntiva - Wikipedia
Leyes de equivalencia