Mjoseh: Página creada con « chapter ‹R6: Formalización y argumentación con Isabelle/HOL› theory R6_sol imports Main begin text ‹----------------------------------…»

2020-03-31T06:50:55Z

Página creada con «<source lang = "isabelle"> chapter ‹R6: Formalización y argumentación con Isabelle/HOL› theory R6_sol imports Main begin text ‹----------------------------------…»

Página nueva

<source lang = "isabelle">
chapter ‹R6: Formalización y argumentación con Isabelle/HOL›

theory R6_sol
imports Main
begin

text ‹---------------------------------------------------------------------
El objetivo de esta es relación formalizar y decidir automáticamente
(con auto, blast, metis, meson o quickcheck) la corrección de los
argumentos.

Para comprobar las formalizaciones, en cada ejercicios se indica
su posición en APLI2 https://www.glc.us.es/apli2 donde las siglas de las
secciones son
+ LP = Lógica proposicional
+ LPO = Lógica de primer orden
›

section ‹Lógica de proposicional›

text ‹---------------------------------------------------------------
Ejercicio 1 [LP-1 en APLI2]. Formalizar, y demostrar la corrección,
del siguiente argumento
Cuando tanto la temperatura como la presión atmosférica permanecen
contantes, no llueve. La temperatura permanece constante. Por lo
tanto, en caso de que llueva, la presión atmosférica no permanece
constante.
Usar T para "La temperatura permanece constante",
P para "La presión atmosférica permanece constante" y
L para "Llueve".
------------------------------------------------------------------›

lemma
"⟦T ∧ P ⟶ ¬L; T⟧ ⟹ L ⟶ ¬P"
by auto

text ‹---------------------------------------------------------------
Ejercicio 2. [LP-3 en APLI2] Formalizar, y demostrar la corrección,
del siguiente argumento
Siempre que un número x es divisible por 10, acaba en 0. El número
x no acaba en 0. Por lo tanto, x no es divisible por 10.
Usar D para "el número es divisible por 10" y
C para "el número acaba en cero".
------------------------------------------------------------------›

lemma
"⟦C ⟶ D; ¬D⟧ ⟹ ¬C"
by auto

text ‹---------------------------------------------------------------
Ejercicio 3. [LP-4 en APLI2] Formalizar, y demostrar la corrección,
del siguiente argumento
En cierto experimento, cuando hemos empleado un fármaco A, el
paciente ha mejorado considerablemente en el caso, y sólo en el
caso, en que no se haya empleado también un fármaco B. Además, o se
ha empleado el fármaco A o se ha empleado el fármaco B. En
consecuencia, podemos afirmar que si no hemos empleado el fármaco
B, el paciente ha mejorado considerablemente.
Usar A: Hemos empleado el fármaco A.
B: Hemos empleado el fármaco B.
M: El paciente ha mejorado notablemente.
------------------------------------------------------------------›

lemma
assumes "A ⟶ (M ⟷ ¬B)"
"A ∨ B"
shows "¬B ⟶ M"
using assms
by auto

text ‹---------------------------------------------------------------
Ejercicio 4. [LP-5 en APLI2] Formalizar, y demostrar la corrección,
del siguiente argumento
Si no está el mañana ni el ayer escrito, entonces no está el mañana
escrito.
Usar M: El mañana está escrito.
A: El ayer está escrito.
------------------------------------------------------------------›

lemma
"¬M ∧ ¬A ⟹ ¬M"
by auto

text ‹---------------------------------------------------------------
Ejercicio 5. [LP-6 en APLI2] Formalizar, y demostrar la corrección,
del siguiente argumento
Me matan si no trabajo y si trabajo me matan. Me matan siempre me
matan.
Usar M: Me matan.
T: Trabajo.
------------------------------------------------------------------›

lemma
"(¬T ⟶ M) ∧ (T ⟶ M) ⟹ M"
by auto

text ‹---------------------------------------------------------------
Ejercicio 6. [LP-7 en APLI2] Formalizar, y demostrar la corrección,
del siguiente argumento
Si te llamé por teléfono, entonces recibiste mi llamada y no es
cierto que no te avisé del peligro que corrías. Por consiguiente,
como te llamé, es cierto que te avisé del peligro que corrías.
Usar T: Te llamé por teléfono.
R: Recibiste mi llamada.
P: Te avisé del peligro que corrías.
------------------------------------------------------------------›

lemma
"T ⟶ R ∧ ¬¬A ⟹ T ⟶ A"
by auto

text ‹---------------------------------------------------------------
Ejercicio 7. [LP-8 en APLI2] Formalizar, y demostrar la corrección,
del siguiente argumento
Si no hay control de nacimientos, entonces la población crece
ilimitadamente; pero si la población crece ilimitadamente,
aumentará el índice de pobreza. Por consiguiente, si no hay control
de nacimientos, aumentará el índice de pobreza.
Usar N: Hay control de nacimientos.
P: La población crece ilimitadamente,
I: Aumentará el índice de pobreza.
------------------------------------------------------------------›

lemma
"⟦¬N ⟶ P; P ⟶ I⟧ ⟹ ¬N ⟶ I"
by auto

text ‹---------------------------------------------------------------
Ejercicio 8. [LP-9 en APLI2] Formalizar, y demostrar la corrección,
del siguiente argumento
Si el general era leal, hubiera obedecido las órdenes, y si era
inteligente las hubiera comprendido. O el general desobedeció las
órdenes o no las comprendió. Luego, el general era desleal o no era
inteligente.
Usar L: El general es leal.
Ob: El general obedece las órdenes.
I: El general es inteligente.
C: El general comprende las órdenes.
------------------------------------------------------------------›

lemma
"⟦(L ⟶ Ob) ∧ (I ⟶ C); ¬Ob ∨ ¬C⟧ ⟹ ¬L ∨ ¬I"
by auto

text ‹---------------------------------------------------------------
Ejercicio 9. [LP-10 en APLI2] Formalizar, y demostrar la corrección,
del siguiente argumento
Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo
haría. Si Dios fuera incapaz de evitar el mal, no sería
omnipotente; si no quisiera evitar el mal sería malévolo. Dios no
evita el mal. Si Dios existe, es omnipotente y no es
malévolo. Luego, Dios no existe.
Usar C: Dios es capaz de evitar el mal.
Q: Dios quiere evitar el mal.
Om: Dios es omnipotente.
M: Dios es malévolo.
P: Dios evita el mal.
E: Dios existe.
------------------------------------------------------------------›

lemma
"⟦C ∧ Q ⟶ P; (¬C ⟶ ¬Om) ∧ (¬Q ⟶ M); ¬P; E ⟶ Om ∧ ¬M⟧ ⟹ ¬E"
by auto

text ‹---------------------------------------------------------------
Ejercicio 10. [LP-12 en APLI2] 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.
------------------------------------------------------------------›

lemma
"⟦A ∨ P ⟶ R ∧ F; F ∨ N ⟶ Or⟧ ⟹ A ⟶ Or"
by auto

text ‹---------------------------------------------------------------
Ejercicio 11. [LP-13 en APLI2] Formalizar, y demostrar la corrección,
del siguiente argumento
Si trabajo gano dinero, pero si no trabajo gozo de la vida. Sin
embargo, si trabajo no gozo de la vida, mientras que si no trabajo
no gano dinero. Por lo tanto, gozo de la vida si y sólo si no gano
dinero.
Usar p: Trabajo
q: Gano dinero.
r: Gozo de la vida.
------------------------------------------------------------------›

lemma
"⟦(p ⟶ q) ∧ (¬p ⟶ r); (p ⟶ ¬r) ∧ (¬p ⟶ ¬q)⟧ ⟹ r ⟷ ¬q"
by auto

section ‹Lógica de primer orden›

text ‹---------------------------------------------------------------
Ejercicio 12. [LPO-2 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------›

lemma
"⟦H(s); ∀x. H(x) ⟶ M(x)⟧ ⟹ M(s)"
by auto

text ‹---------------------------------------------------------------
Ejercicio 13. [LPO-3 en APLI2] 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
------------------------------------------------------------------›

lemma
"(∃x. I(x)) ∧ (∃x. T(x)) ⟹ ∃x. I(x) ∧ T(x)"
quickcheck
oops

text ‹El argumento es incorrecto como muestra el siguiente contraejemplo:
I = {a⇩1}
x = a⇩1
T = {a⇩2}
xa = a⇩2
›

text ‹---------------------------------------------------------------
Ejercicio 14. [LPO-4 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor
------------------------------------------------------------------›

lemma
"⟦∀x. P(x) ⟶ V(x);
∀x y. V(x) ∧ V(y) ⟶ x=y;
∀x y. P(x) ∧ P(y) ⟶ x=y⟧
⟹ ∃x. P(x) ∧ (∀y. P(y) ⟶ x=y)"
quickcheck
oops

text ‹El argumento es incorrecto como muestra el siguiente contraejemplo:
V = {}
P = {} ›

text ‹---------------------------------------------------------------
Ejercicio 15. [LPO-5 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------›

lemma
"⟦∀x. E(x) ∧ ¬V(x) ⟶ (∃y. A(y) ∧ Ca(y,x));
∃x. Co(x) ∧ E(x) ∧ (∀y. Ca(y,x) ⟶ Co(y));
¬(∃x. Co(x) ∧ V(x))⟧
⟹ ∃x. A(x) ∧ Co(x)"
by metis

text ‹---------------------------------------------------------------
Ejercicio 16. [LPO-6 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------›

lemma
"⟦T(j,m); T(j,p)⟧ ⟹ ∃x. T(x,m) ∧ T(x,p)"
by auto

text ‹---------------------------------------------------------------
Ejercicio 17. [LPO-8 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------›

lemma
assumes "(∃x. Pu(x)) ⟶ (∀x. Pr(x) ⟶ A(x))"
"∀x. A(x) ⟶ (∀y. D(y,x) ⟶ S(y))"
"∃x. Pu(x)"
"Pr(t)"
shows "∀x. D(x,t) ⟶ S(x)"
using assms
by auto

text ‹---------------------------------------------------------------
Ejercicio 18. [LPO-9 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Quien intente entrar en un país y no tenga pasaporte, encontrará
algún aduanero que le impida el paso. A algunas personas
motorizadas que intentan entrar en un país le impiden el paso
únicamente personas motorizadas. Ninguna persona motorizada tiene
pasaporte. Por tanto, ciertos aduaneros están motorizados.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------›

lemma
assumes "∀x. E(x) ∧ ¬P(x) ⟶ (∃y. A(y) ∧ I(y,x))"
"∃x. M(x) ∧ E(x) ∧ (∀y. I(y,x) ⟶ M(y))"
"∀x. M(x) ⟶ ¬P(x)"
shows "∃x. A(x) ∧ M(x)"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 19. [LPO-10 en APLI2] 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
------------------------------------------------------------------›

lemma
assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
"∀x. E(x) ⟶ ¬Ap(j,x)"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 20. [LPO-11 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------›

lemma
assumes "∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x)"
"∃x. A(x) ∧ V(x) ∧ ¬L(x)"
shows "∃x. A(x) ∧ ¬G(x)"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 21. [LPO-12 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------›

lemma
assumes "∀x y. C(x,y) ⟶ A(x,y) ∨ I(x)"
"∀x. I(x) ⟶ ¬R(x)"
"∀x. E(x) ⟶ C(x,m) ∧ ¬A(x,m)"
shows "∀x. ¬E(x) ∨ (C(x,m) ∧ ¬R(x))"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 22. [LPO-13 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------›

lemma
assumes "∀x. ¬R(x) ⟶ R(p(x))"
shows "∃x. R(x) ∧ R(p(p(x)))"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 23. [LPO-14 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------›

lemma
assumes "∀x. D(x) ∧ (∃y. S(y) ∧ E(x,y)) ⟶ L(x)"
"∀x. E(x,x) ⟶ L(x)"
"¬(∃x. D(x) ∧ E(x,x))"
shows "¬(∃x. D(x) ∧ (∃y. S(y) ∧ E(x,y)))"
quickcheck
oops

text ‹El argumento es incorrecto como muestra el siguiente contraejemplo:
Quickcheck found a counterexample:
D = {a2}
S = {a1}
E = {(a2, a1)}
L = {a2}
x = a2 ›

text ‹---------------------------------------------------------------
Ejercicio 24. [LPO-15 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------›

lemma
assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
"A(a)"
"¬Ob(b,a)"
shows "¬R(b)"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 25. [LPO-16 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------›

lemma
assumes "∃x. ∀y. ¬C(x,y) ⟶ (∃z. T(z) ∨ P(z,y))"
"∀x. ∃y. ¬C(x,y)"
"∀x y. ¬P(x,y)"
shows "∃x. T(x)"
using assms
by auto

text ‹---------------------------------------------------------------
Ejercicio 26. [LPO-17 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------›

lemma
assumes "(∀x. A(x,a)) ⟶ (∀x. A(x,b))"
"(∃x. D(x) ∧ A(x,a) ∧ A(x,b)) ⟶ (∀x. A(x,a))"
"(∀x. ¬A(x,b)) ⟶ (∀x. D(x) ⟶ ¬A(x,a))"
"¬A(m,b) ⟶ (∀x. ¬A(x,b))"
shows "D(m) ∧ A(m,a) ⟶ (∀x. A(x,a) ∧ A(x,b))"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 27. [LPO-18 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------›

lemma
assumes "∀x. P(x) ∧ ¬N(x) ⟶ (∃y. D(y) ∧ M(y,x))"
"∃x. P(x) ∧ B(x) ∧ (∀y. M(y,x) ⟶ B(y))"
"¬(∃x. P(x) ∧ M(x,x))"
"¬(∃x. B(x) ∧ N(x))"
shows "∃x. D(x) ∧ B(x)"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 28. [LPO-19 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------›

lemma
assumes "∀x y. He(x,y) ⟶ He(y,x)"
"∀x. ∃y. Hi(x,y)"
"∀x y z. Hi(x,y) ∧ He(z,y) ⟶ ¬Hi(x,z)"
"∀x y. Hi(x,y) ⟶ (∀z. He(z,x) ⟶ Hi(z,y))"
"∀x. ¬Hi(x,x) ∧ ¬He(x,x)"
"He(A,L)"
"He(a,m)"
"Hi(a,A)"
shows "¬Hi(m,L)"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 29. [LPO-20 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------›

lemma
assumes "∀x. B(x) ∧ (∃y. B(y) ∧ A(x,y)) ⟶ (∀z. B(z) ⟶ A(z,x))"
"B(g)"
"B(l)"
"B(p)"
"B(c)"
"A(g,c)"
shows "A(p,l)"
using assms
by meson

text ‹---------------------------------------------------------------
Ejercicio 30. [LPO-21 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------›

lemma
assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
"C(c)"
shows "¬(∃x. A(c,x))"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 31. [LPO-22 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------›

lemma
assumes "∀x. (∀y. F(y) ⟶ D(x,y)) ⟶ (∀y. P(y) ⟶ D(x,y))"
"∃x y. P(y) ∧ ¬D(x,y)"
shows "∃x. F(x) ∧ ¬(∀y. D(y,x))"
using assms
by blast

text ‹---------------------------------------------------------------
Ejercicio 32. [LPO-23 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------›

lemma
assumes "∀x. H(x) ∧ P(x) ⟶ (∀y. P(y) ⟶ A(x,y))"
shows "∀x. H(x) ∧ P(x) ⟶ A(x,x)"
using assms
by auto

text ‹---------------------------------------------------------------
Ejercicio 33. [LPO-24 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------›

lemma
assumes "¬(∃x. P(x) ∧ R(x))"
"∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
shows "P(a) ⟶ Q(a)"
using assms
by auto

text ‹---------------------------------------------------------------
Ejercicio 34. [LPO-25 en APLI2] Formalizar, y decidir la corrección,
del siguiente argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------›

lemma
assumes
"∀x. L(x) ⟶ A(x)"
"∀x. Z(x) ⟶ A(x)"
"∀x. Pa(x) ⟶ A(x)"
"∀x. Or(x) ⟶ A(x)"
"∀x. Ca(x) ⟶ A(x)"
"∃x. L(x)"
"∃x. Z(x)"
"∃x. Pa(x)"
"∃x. Or(x)"
"∃x. Ca(x)"
"∃x. S(x)"
"∀x. S(x) ⟶ Pl(x)"
"∀x. A(x) ⟶
(∀y. Pl(y) ⟶ Co(x,y)) ∨
(∀y. A(y) ∧ M(y,x) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(x,y))"
"∀x y. Pa(y) ∧ (Ca(x) ∨ Or(x)) ⟶ M(x,y)"
"∀x y. Pa(x) ∧ Z(y) ⟶ M(x,y)"
"∀x y. Z(x) ∧ L(y) ⟶ M(x,y)"
"∀x y. L(x) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(x,y)"
"∀x y. Pa(x) ∧ Or(y) ⟶ Co(x,y)"
"∀x y. Pa(x) ∧ Ca(y) ⟶ ¬Co(x,y)"
"∀x. Or(x) ∨ Ca(x) ⟶ (∃y. Pl(y) ∧ Co(x,y))"
shows
"∃x y. A(x) ∧ A(y) ∧ (∃z. S(z) ∧ Co(y,z) ∧ Co(x,y))"
using assms
by meson

end

</source>

Rel 6 - Historial de revisiones

Mjoseh: Protegió «Rel 6» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹R6: Formalización y argumentación con Isabelle/HOL› theory R6_sol imports Main begin text ‹----------------------------------…»

← Revisión anterior	Revisión del 06:51 31 mar 2020
(Sin diferencias)