RA12 Relación 6
De DAO (Demostración asistida por ordenador)
Revisión del 20:24 1 abr 2013 de Jalonso (discusión | contribuciones) (Página creada con '<source lang="isar"> header {* R6: Argumentación en lógica de primer orden con igualdad *} theory R6 imports Main begin text {* ------------------------------------------...')
header {* R6: Argumentación en lógica de primer orden con igualdad *}
theory R6
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar y decidir la corrección
de los argumentos. En el caso de que sea correcto, demostrarlo usando
sólo las reglas básicas de deducción natural de la lógica de primer
orden (sin usar el método auto). En el caso de que sea incorrecto,
calcular un contraejemplo con QuickCheck.
Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· 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
· excluded_middle: ¬P ∨ 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, además, siquientes reglas que demostramos a continuación.
*}
text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar, y decidir la corrección, del siguiente
argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar, y decidir la corrección, del siguiente
argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar, y decidir la corrección, del siguiente
argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}
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
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar, y decidir la corrección, del siguiente
argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar, y decidir la corrección, del siguiente
argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar, y decidir la corrección, del siguiente
argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar, y decidir la corrección, del siguiente
argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar, y decidir la corrección, del siguiente
argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar, y decidir la corrección, del siguiente
argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}
end