Posterior: Algoritmo de Davis y Arriba: Procedimientos de demostración automática Anterior: Algoritmo de Wang

Representación matricial

Éste es un procedimiento para decidir cuándo una proposición dada en FC es o no contradicción. Representaremos a una proposición $\phi$ por su matriz de literales
$M_{\phi}= \left(\ell_{ij} \right)_{1\leq i\leq m; 1\leq j\leq \mbox{\scriptsize long}(i)}$. $m$ es el número de cláusulas en la FC de $\phi$. $\mbox{\rm long}(i)$ es la longitud de la $i$-ésima cláusula. Usaremos las siguientes nociones:

Camino.

Sucesión de literales $\ell_{1,\pi(1)} \ldots \ell_{n,\pi(n)}$, donde para cada $i\leq m$, $1 \leq \pi(i) \leq \mbox{\rm long}(i).$

Camino complementado.

Camino donde aparecen $x$ y $\neg x$, para alguna literal $x$.

Procedimiento 4.7 (Representación matricial)  


Entrada:

Salida:




Algoritmo:

1. Comenzando con el camino a la extrema izquierda, $\ell_{1,1} \ldots \ell_{n,1}$, hacemos variar más rápidamente los dígitos más a la derecha.
2. Al reconocer a un camino como complementado omitiremos a todos los caminos que pasen por la pareja que lo hace complementado.
   1. Si acaso todos los caminos son complementados entonces $\phi$ es contradicción.
   2. En otro caso, al hacer verdaderas a todas las literales que aparecen en un camino no complementado tendremos una asignación que hace a $\phi$ verdadera. $\bullet$

Posterior: Algoritmo de Davis y Arriba: Procedimientos de demostración automática Anterior: Algoritmo de Wang