Diferencia entre revisiones de «Relación 1»
De Razonamiento automático (2010-11)
| Línea 20: | Línea 20: | ||
lemma "A ∧ B ⟶ A ∨ B" | lemma "A ∧ B ⟶ A ∨ B" | ||
| − | + | proof | |
| + | assume "A ∧ B" | ||
| + | hence "A" .. | ||
| + | thus "A ∨ B" .. | ||
| + | qed | ||
lemma "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)" | lemma "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)" | ||
Revisión del 17:57 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"
proof
assume "A ∧ B"
hence "A" ..
thus "A ∨ B" ..
qed
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