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

2018-07-16T11:11:16Z

Texto reemplazado: «isar» por «isabelle»

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

2017-01-26T07:29:30Z

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

Jalonso: Página creada con ' chapter {* R10: Formalización y argumentación con Isabelle/HOL } theory R10_Formalizacion_y_argmentacion imports Main begin text { ----------------...'

2017-01-26T07:29:12Z

Página creada con '<source lang="isar"> chapter {* R10: Formalización y argumentación con Isabelle/HOL *} theory R10_Formalizacion_y_argmentacion imports Main begin text {* ----------------...'

Página nueva

<source lang="isar">
chapter {* R10: Formalización y argumentación con Isabelle/HOL *}

theory R10_Formalizacion_y_argmentacion
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta es relación formalizar y demostrar la corrección
de los argumentos automáticamente y detalladamente usando sólo las reglas
básicas de deducción natural.

· 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, no_ex y no_para_todo 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

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

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
argumento
Si la válvula está abierta o la monitorización está preparada,
entonces se envía una señal de reconocimiento y un mensaje de
funcionamiento al controlador del ordenador. Si se envía un mensaje
de funcionamiento al controlador del ordenador o el sistema está en
estado normal, entonces se aceptan las órdenes del operador. Por lo
tanto, si la válvula está abierta, entonces se aceptan las órdenes
del operador.
Usar A : La válvula está abierta.
P : La monitorización está preparada.
R : Envía una señal de reconocimiento.
F : Envía un mensaje de funcionamiento.
N : El sistema está en estado normal.
O : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar, y decidir la corrección, del siguiente
argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar, y decidir la corrección, del siguiente
argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar, y decidir la corrección, del siguiente
argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar, y decidir la corrección, del siguiente
argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

end
</source>

← Revisión anterior		Revisión del 11:11 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	chapter {* R10: Formalización y argumentación con Isabelle/HOL *}		chapter {* R10: Formalización y argumentación con Isabelle/HOL *}

← Revisión anterior	Revisión del 07:29 26 ene 2017
(Sin diferencias)

R10 - Historial de revisiones

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

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

Jalonso: Página creada con ' chapter {* R10: Formalización y argumentación con Isabelle/HOL *} theory R10_Formalizacion_y_argmentacion imports Main begin text {* ----------------...'

Jalonso: Página creada con ' chapter {* R10: Formalización y argumentación con Isabelle/HOL } theory R10_Formalizacion_y_argmentacion imports Main begin text { ----------------...'