Relación 5 - Historial de revisiones

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

2018-07-16T12:41:08Z

Texto reemplazado: «Isar» por «isabelle»

Angruigon2: 1

2016-04-26T12:01:47Z

Marherfer6 en 09:11 24 abr 2016

2016-04-24T09:11:17Z

Angruigon2: cambio de notacion

2016-04-19T14:42:22Z

cambio de notacion

Angruigon2: cambio del dos por el 7

2016-04-19T14:36:11Z

cambio del dos por el 7

Angruigon2: 2 con demostración ,6,7

2016-04-16T10:36:15Z

2 con demostración ,6,7

Mjoseh: Página creada con ' header {* R5: Argumentación en lógica de primer orden } theory R5 imports Main begin text { -----------------------------------------------------...'

2016-04-06T18:45:08Z

Página creada con '<source lang = "Isar"> header {* R5: Argumentación en lógica de primer orden *} theory R5 imports Main begin text {* -----------------------------------------------------...'

Página nueva

<source lang = "Isar">
header {* R5: Argumentación en lógica de primer orden *}

theory R5
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar en lógica de primer orden
argumentos expresados en lenguaje natural.

Antes de escribir la soluciones, comprobar con APLI2 la corrección de la
formalización.

Una vez formalizadas, probar que el razonamiento es correcto, o refutarlo
mediante un contraejemplo.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar el 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 2. Formalizar el 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar el 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar el 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar el 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
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar el 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 7. Formalizar el 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
------------------------------------------------------------------ *}

section {* Ejercicios con igualdad *}

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar el 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 9. Formalizar el 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 10. Formalizar el 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
------------------------------------------------------------------ *}

end
</source>

← Revisión anterior		Revisión del 12:41 16 jul 2018
Línea 1:		Línea 1:
−	<source lang = "~~Isar~~">	+	<source lang = "isabelle">
	header {* R5: Argumentación en lógica de primer orden *}		header {* R5: Argumentación en lógica de primer orden *}

@@ Línea 93: / Línea 93: @@
         j       para Juanito
    ------------------------------------------------------------------ *}
-lemma ejercicio9
+lemma ejercicio6
 assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
            "∀x. E(x) ⟶ ¬Ap(j,x)"

@@ Línea 41: / Línea 41: @@
 : "(¬(∃x. P(x))) ∨ (∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y))))"
 shows "∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y)))"
+quickcheck
-proof -
+oops
 text {* ---------------------------------------------------------------
    Ejercicio 3. Formalizar el siguiente argumento
@@ Línea 134: / Línea 116: @@
 : "∀x. (Co(x)⟶ ¬V(x))"
 shows "∃x. (A(x) ∧ Co(x))"
-oops
+proof -
 section {* Ejercicios con igualdad *}

@@ Línea 55: / Línea 55: @@
         V(x)  para x ha cometido crímenes vergonzoso
    ------------------------------------------------------------------ *}
 text {* ---------------------------------------------------------------
@@ Línea 67: / Línea 87: @@
         a       para Alvaro
    ------------------------------------------------------------------ *}
@@ Línea 80: / Línea 114: @@
         a    para el tesorero del club
     ------------------------------------------------------------------ *}
 text {* ---------------------------------------------------------------