Posterior: Encadenamiento hacia atrás Arriba: Procedimientos de demostración automática Anterior: Pruebas por refutación

Tablas de verdad

Procedimiento 4.1 (Tablas de verdad)   Dada una proposición
$\phi(x_1,\ldots,x_n)$ con $n$ variables proposicionales, enumere $\mbox{\rm Dos}^n=\{0,1\}^n$ y evalúe el valor de verdad de $\phi$ para cada una de las $2^n$ asignaciones, cada una de las cuales se colocará en uno de dos arreglos de asignaciones: Aquel correspondiente a las asignaciones que satisfacen la proposición y aquel correspondiente a las asignaciones que refutan a la proposición.

La complejidad de este procedimiento es de $O(2^n)$ evaluaciones de formas proposicionales. Con él se obtiene también a las formas normales: La forma normal conjuntiva, FNC, es precisamente la conjunción de las cláusulas correspondientes a las asignaciones que refutan a la proposición y la forma normal disyuntiva, FND, es precisamente la disyunción de las frases correspondientes a las asignaciones que satisfacen a la proposición.