Relación 10
De Razonamiento automático (2016-17)
Revisión del 16:32 28 ene 2017 de Ivamenjim (discusión | contribuciones)
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.
------------------------------------------------------------------ *}
(* ivamenjim *)
(* Buscando, he detectado que 'O' es un carácter especial en Isabelle y que forma parte de su
sintaxis pre-definida, por lo que da problemas a la hora de formalizar y demostrar
el argumento planteado. Por lo tanto, en su lugar he usado "AO: Se aceptan órdenes del operador" *)
lemma ejercicio_1:
assumes 1: "(A ∨ P) ⟶ (R ∧ F)"
assumes 2: "(F ∨ N) ⟶ AO"
shows "A ⟶ AO"
proof -
{assume 3: "A"
have 4: "A ∨ P" using 3 by (rule disjI1)
have 5: "R ∧ F" using 1 4 by (rule mp)
have 6: "F" using 5 by (rule conjunct2)
have 7: "F ∨ N" using 6 by (rule disjI1)
have 8: "AO" using 2 7 by (rule mp)}
then show "A ⟶ AO" by (rule impI)
qed
(*danrodcha*)
lemma ej_1:
assumes "A ∨ P ⟶ R ∧ F" and
"F ∨ N ⟶ OK"
shows "A ⟶ OK"
proof (rule impI)
{assume "A"
hence "A ∨ P" by (rule disjI1)
with assms(1) have "R ∧ F" by (rule mp)
hence "F" by (rule conjE)
hence "F ∨ N" by (rule disjI1)
with assms(2) show "OK" by (rule mp)}
qed
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
------------------------------------------------------------------ *}
(* ivamenjim ferrenseg danrodcha *)
lemma ejercicio_2:
assumes "(∃x. I(x)) ∧ (∃x. T(x))"
shows "∃x. (I(x) ∧ T(x))"
quickcheck
oops
(* Encontrando el contraejemplo:
I = {a1}
x = a1
T = {a2}
xa = a2
*)
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
------------------------------------------------------------------ *}
(* ivamenjim *)
lemma ejercicio_3:
assumes 1: "∀x y. P(x,y) ⟶ (∀z. (H(z,y) ⟶ P(x,z)))"
assumes 2: "H(j,l)"
assumes 3: "P(c,l)"
shows "P(c,j)"
proof -
have 4 : "∀y. P(c,y) ⟶ (∀z. (H(z,y) ⟶ P(c,z)))" using 1 by (rule allE)
have 5 : "P(c,l) ⟶ (∀z. (H(z,l) ⟶ P(c,z)))" using 4 by (rule allE)
then have 6 : "(∀z. (H(z,l) ⟶ P(c,z)))" using 3 by (rule mp)
have 7 : "H(j,l) ⟶ P(c,j)" using 6 by (rule allE)
then show "P(c,j)" using 2 by (rule mp)
qed
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
------------------------------------------------------------------ *}
(* ivamenjim *)
lemma ejercicio_5:
assumes 1: "e(h) = r"
assumes 2: "h = m"
shows "e(m) = r"
proof -
have 3: "e(h) = e(m)" using 2 by (rule arg_cong)
have 4: "e(m) = e(h)" using 3 by (rule sym)
then show "e(m) = r" using 1 by (rule trans)
qed
end