Ver el código de «RA12 Relación 6» - DAO (Demostración asistida por ordenador)

<source lang="isabelle">
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
</source>