Teorema de Corrección del Método de Árboles en Lógica de Predicados
Enviado por Programa Chuletas y clasificado en Matemáticas
Escrito el en 
con un tamaño de 2,49 KB
Teorema de corrección del método de árboles de la lógica de predicados
Siempre que se clasifica una inferencia como válida, al obtenerse un árbol cerrado, esa clasificación es semánticamente correcta. Lo cual equivale a decir que: si la lista inicial es satisfacible, el árbol nunca se cierra.
Lema de corrección
Siempre que se aplica una regla a una rama satisfacible, al menos una de las ramas en que se prolonga sigue siendo satisfacible y, por tanto, abierta.
Para probar este lema (y con ello el teorema de corrección) basta verificar que cuando las fbf (fórmulas bien formadas) de una rama son verdaderas para una interpretación I, y se aplica una regla, al menos una de las listas de conclusiones, añadida a la rama, es verdadera para I o para alguna variante nominal de I.
Esto se comprueba considerando las reglas de inferencia sucesivamente:
- Caso 1. Las reglas veritativo-funcionales: Obvio, por el lema de adecuación de estas reglas.
- Caso 2. La regla de diversidad: De acuerdo con la interpretación semántica del signo “=”, para cualquier interpretación I, I(k=k)=V y, por tanto, I(k≠k)=F. Luego el lema se cumple vacuamente, al ser falso su antecedente.
- Caso 3. La regla de identidad: Si la rama contiene la fbf k=j y la fbf Pk que son por tanto V bajo I, obviamente la fbf Pj también será V bajo I.
- Caso 4. Las reglas para cuantificadores negados: (Lo demostramos para la negación del universal; para la del existencial la prueba es prácticamente igual). Si la rama contiene la fbf ¬∀v P(v) que es por tanto V bajo I, obviamente la fbf ∃v ¬P(v) también será V bajo I.
- Caso 5. La regla para el cuantificador universal: Si la rama contiene la fbf ∀v P(v) que es por tanto V bajo I, la fbf Pk (para cualquier constante k) también será V bajo I.
- Caso 6. La regla para el cuantificador existencial: Si la rama contiene la fbf ∃v P(v) que es por tanto V bajo I, la fbf Pk también será V para alguna variante nominal de I.
Así quedan demostrados el lema y el teorema de corrección.