Diferencia entre revisiones de «Relación 1»
De Razonamiento automático (2010-11)
(Página creada con '<pre> header {* 1ª relación de ejercicios *} theory Relacion_1 imports Main begin text {* --------------------------------------------------------------------- Demostr...') |
|||
| Línea 1: | Línea 1: | ||
| − | < | + | <source lang="isabelle"> |
header {* 1ª relación de ejercicios *} | header {* 1ª relación de ejercicios *} | ||
| Línea 53: | Línea 53: | ||
end | end | ||
| − | </ | + | </source> |
Revisión del 10:45 1 feb 2011
header {* 1ª relación de ejercicios *}
theory Relacion_1
imports Main
begin
text {*
---------------------------------------------------------------------
Demostrar los siguientes lemas usando sólo las reglas básicas de
deducción natural de la lógica proposicional.
---------------------------------------------------------------------
*}
lemma I: "A ⟶ A"
oops
lemma "A ∧ B ⟶ B ∧ A"
oops
lemma "A ∧ B ⟶ A ∨ B"
oops
lemma "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
oops
lemma K: "A ⟶ (B ⟶ A)"
oops
lemma S: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
oops
lemma "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
oops
lemma "¬¬A ⟶ A"
oops
lemma "A ⟶ ¬¬A"
oops
lemma "(¬A ⟶ B) ⟶ (¬B ⟶ A)"
oops
lemma "((A ⟶ B) ⟶ A) ⟶ A"
oops
lemma "A ∨ ¬A"
oops
lemma "(¬(A ∧ B)) = (¬A ∨ ¬B)"
oops
end