Posterior: Resolución lineal
Arriba: Procedimientos de demostración automática
Anterior: Representación matricial
Dada
, sea
la matriz de literales.
aparece como LITERAL AISLADA si hay una cláusula que consiste
sólo de
, es decir, si hay un renglón de
que consta tan solo
de
.
aparece como LITERAL PURA si, habiendo aparecido ella en
, no aparece
.
Posterior: Resolución lineal
Arriba: Procedimientos de demostración automática
Anterior: Representación matricial
Guillermo Morales-Luna
2004-07-27