WikiSysop: Texto reemplazado: «"isar"» por «"isabelle"»

2018-07-16T08:18:04Z

Texto reemplazado: «"isar"» por «"isabelle"»

Jalonso: Protegió «R9» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2014-12-18T10:10:45Z

Protegió «R9» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* R9: Deducción natural en Isabelle/HOL } theory R9 imports Main begin text { Demostrar o refutar los siguientes lemas usando sólo las regl...'

2014-12-18T10:10:28Z

Página creada con '<source lang="isar"> header {* R9: Deducción natural en Isabelle/HOL *} theory R9 imports Main begin text {* Demostrar o refutar los siguientes lemas usando sólo las regl...'

Página nueva

<source lang="isar">
header {* R9: Deducción natural en Isabelle/HOL *}

theory R9
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, de los
cuantificadores y de la igualdad:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P

· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
*}

text {*
Se usarán las reglas notnotI, mt y not_ex que demostramos a continuación.
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ∨ q, ¬q ⊢ p
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
{∀x y z. R x y ∧ R y z ⟶ R x z,
∀x. ¬(R x x)}
⊢ ∀x y. R x y ⟶ ¬(R y x)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)⟧
⊢ ∃z. P (f a) z (f (f a))
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
{∀y. Q a y,
∀x y. Q x y ⟶ Q (s x) (s y)}
⊢ ∃z. Qa z ∧ Q z (s (s a))
------------------------------------------------------------------ *}

end
</source>

← Revisión anterior		Revisión del 08:18 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R9: Deducción natural en Isabelle/HOL *}		header {* R9: Deducción natural en Isabelle/HOL *}

← Revisión anterior	Revisión del 10:10 18 dic 2014
(Sin diferencias)

R9 - Historial de revisiones

WikiSysop: Texto reemplazado: «"isar"» por «"isabelle"»

Jalonso: Protegió «R9» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* R9: Deducción natural en Isabelle/HOL *} theory R9 imports Main begin text {* Demostrar o refutar los siguientes lemas usando sólo las regl...'

Jalonso: Página creada con ' header {* R9: Deducción natural en Isabelle/HOL } theory R9 imports Main begin text { Demostrar o refutar los siguientes lemas usando sólo las regl...'