Tengo que hacer diferentes ejercicios relacionados con el método de tableau. Por ejemplo, necesito mostrar si una fórmula $X$ es una tautología o no. Por lo tanto, ¿tengo que verificar si todas las ramas de $\neg X$ están cerradas, verdad? ¿Pero qué hago si las ramas no se cierran? ¿He encontrado una asignación booleana tal que $X$ sea falsa?
Y también tengo un tipo diferente de ejercicio con no solo una fórmula, sino un conjunto de fórmulas, ¿tengo que negar todas ellas y usar el método de tableau de nuevo?
Realmente estoy confundido en este momento y agradecería cualquier ayuda!
Respuesta
¿Demasiados anuncios?
Correcto.
El método del tableau es un procedimiento de refutación; si todas las ramas del tableau se cierran, entonces la fórmula inicial es insatisfactible.
Por lo tanto, si comenzamos con $\lnot X$ y el tableau se cierra, esto significa que $\lnot X$ es insatisfactible, es decir, $X$ es una tautología.
Si el procedimiento termina y una rama no se cierra, esta rama determina una asignación de valores de verdad a los átomos que satisfacen la fórmula inicial: en nuestro caso, $\lnot X$.
Pero si $\lnot X$ es satisfecho por una asignación adecuada, esto significa que, para esa asignación, $X$ es falsificado, y por lo tanto $X$ no es una tautología.
Con un conjunto de fórmulas, podemos tener dos tipos de preguntas:
(i) verificar si la última (la conclusión) es implicada por las otras (las premisas).
En este caso, tenemos que considerar las premisas con la negación de la conclusión; si el tableau se cierra, este hecho prueba que la conclusión es implicada por las premisas.
(ii) verificar si el conjunto de fórmulas es satisfactible.
En este caso aplicamos el tableau al conjunto original de fórmulas; si el tableau está abierto, esto significa que el conjunto de fórmulas es satisfactible.
