Posterior: Representación matricial
Arriba: Procedimientos de demostración automática
Anterior: Transformación a forma normal
Procedimiento 4.6 (Algoritmo de Wang)
Entrada:
Salida:
Algoritmo:
- Coloque al inicio de
una proposición
que no sea una literal.
- Sea
esta proposición y sea
el resto de
.
- Transforme
a una proposición equivalente, sólo con
conectivos
.
- Revise el conectivo principal de
:
- Si éste es
, entonces
. Sustituya
a
por la lista
(donde
es la
concatenación de listas). Invoque a este mismo algoritmo con la
sustitución hecha. Si obtiene una respuesta afirmativa
es
una tautología.
- Si éste es
, entonces
. Invoque este
mismo algoritmo, una vez con el argumento
y otra con
el argumento
.
Si en ambos casos obtiene una respuesta afirmativa entonces
es una tautología.
- Si éste es
, entonces
. Invoque este mismo
algoritmo, con el argumento
. Si obtiene una
respuesta afirmativa entonces
es una tautología.
- Si todas las proposiciones en
son literales, considere ahora
a
.
- Coloque al inicio de
una proposición que no sea una
literal.
- Sea
esta proposición y sea
el resto de
.
- Transforme
a una proposición equivalente, sólo con
conectivos
.
- Revise el conectivo principal de
.
- Si éste es
, entonces
. Sustituya a
por la lista
. Invoque a este mismo algoritmo
con la sustitución hecha. Si obtiene una respuesta afirmativa
es una tautología.
- Si éste es
, entonces
. Invoque
este mismo algoritmo, una vez con el argumento
y
otra con el argumento
. Si en ambos casos obtiene
una respuesta afirmativa
es una tautología.
- Si éste es
, entonces
. Invoque este mismo
algoritmo, con el argumento
. Si obtiene una
respuesta afirmativa entonces
es una tautología.
- Si todas las proposiciones en
también son literales, continúe con el paso siguiente.
- Vea si acaso hay una literal común a
y a
.
- En este caso
es una tautología.
- En caso contrario, no lo es, de hecho al hacer
a las literales en
verdaderas y a las literales en
falsas
obtenemos una asignación que hace a
falsa.
- En un inicio, si se da una proposición
, al invocar el
algoritmo con el argumento
, donde
es
la lista vacía, entonces el algoritmo descrito nos dice si
es o no una tautología.
De hecho, el algoritmo da más. Por su descripción
vemos que gradualmente irá definiendo una estructura arbórea
cuyos nodos corresponden a proposiciones. Si al final descartamos a
las ``hojas'' que son tautologías, la conjunción de las que nos
queden será una FC equivalente a
.
Posterior: Representación matricial
Arriba: Procedimientos de demostración automática
Anterior: Transformación a forma normal
Guillermo Morales-Luna
2004-07-27