R9
De Lógica matemática y fundamentos (2017-18)
Relación 9: Resolución proposicional
Ejercicio 1. Dadas las fórmulas A : (s → p) ∨ (t → q) y B : (s → q) ∨ (t → p), se pide:
- Probar que A ⊧ B, mediante resolución proposicional.
- Describir, razonadamente, todos los modelos de A y, a continuación, probar nuevamente que A ⊧ B, utilizando la definición de consecuencia lógica.
- ¿Es ¬B → ¬A una tautología?
Solución:
Ejercicio 2. Consideremos la fórmula proposicional A : (r → p) ∧ (¬r → q ∨ s) → p ∨ q ∨ s y el conjunto de fórmulas U = {r ⇔ p ∨ q, s → p, ¬s ∧ ¬r → s ∨ t}.
- Probar, mediante tableros semánticos, que A es una tautología.
- Probar, razonadamente, que U es consistente, mostrando para ello un modelo de U.
- Probar, mediante resolución, que U ⊧ ¬p → (q ∨ t).
- Sea B la fórmula (¬p → (q ∨ t)). ¿Podemos eliminar alguna fórmula de U de
manera que la fórmula B sea consecuencia lógica del conjunto de fórmulas restante?
Solución:
Ejercicio 3.
Decidir, mediante resolución, si r es consecuencia lógica de
{p ⇔ q, ¬p → r, ¬ s ∧ ¬ t → q, ¬ s ∧ t}
En el caso que no lo sea, construir un contramodelo a partir de la resolución.
Solución: