Diferencia entre revisiones de «Rel 2»
De Razonamiento automático (2010-11)
m (Protegió «Rel 2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))) |
|||
| Línea 1: | Línea 1: | ||
| − | <source lang=" | + | <source lang="isabelle"> |
header {* 2ª relación de ejercicios *} | header {* 2ª relación de ejercicios *} | ||
Revisión actual del 09:49 16 jul 2018
header {* 2ª relación de ejercicios *}
theory Relacion_2
imports Main
begin
text {*
Demostrar o refutar los siguientes lemas usando sólo las reglas
básicas de deducción natural de la lógica proposicional y de la lógica
de predicados (allI, allE, exI y exE).
*}
lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
oops
lemma "(∀x. P x ⟶ Q) = ((∃x. P x) ⟶ Q)"
oops
lemma "((∀ x. P x) ∧ (∀ x. Q x)) = (∀ x. (P x ∧ Q x))"
oops
lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))"
oops
lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))"
oops
lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops
lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
oops
end