Diferencia entre revisiones de «Rel 1»
De Razonamiento automático (2010-11)
m (Protegió «Rel 1» ([edit=sysop] (indefinido) [move=sysop] (indefinido))) |
m (Texto reemplazado: «"isar"» por «"isabelle"») |
||
| Línea 1: | Línea 1: | ||
| − | <source lang=" | + | <source lang="isabelle"> |
header {* 1ª relación de ejercicios *} | header {* 1ª relación de ejercicios *} | ||
Revisión actual del 09:48 16 jul 2018
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