Relación 1

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

De Razonamiento automático (2010-11)