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

2020-05-04T09:53:41Z

Protegió «T1» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)› theory Tarea1 imports Main begin text ‹ Apellidos: Nombre: ›…»

2020-05-04T09:53:30Z

Página creada con «<source lang = "isabelle"> text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)› theory Tarea1 imports Main begin text ‹ Apellidos: Nombre: ›…»

Página nueva

<source lang = "isabelle">

text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)›

theory Tarea1
imports Main
begin

text ‹
Apellidos:
Nombre:
›

text ‹Sustituye la palabra uvus por tu usuario de la Universidad de
Sevilla y graba el fichero con dicho usuario.thy
›

text ‹Nota: En las demostraciones se pueden las reglas básicas de
deducción natural de la lógica proposicional, de los cuantificadores
y de la igualdad:
· 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
· excluded_middle: (¬P ∨ P)

· allE: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allI: (⋀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⟧ ⟹ c = 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

También se pueden usar las reglas notnotI y mt que demostramos a
continuación.
›

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text ‹Ejercicio: Formalizar la siguiente argumentación

Hay un profesor que agrada a todos los estudiantes a los que
agrada al menos un profesor. A todo estudiante le agrada uno u otro
profesor.
(a) Demostrar que hay un profesor que agrada a todos los estudiantes.
(b) ¿Hay un profesor que no agrade a ningún estudiante?

Simbología: P(x): x es un profesor, E(x): x es estudiante, A(x,y):
a x le agrada y.

Notas:
(1) No usar ninguno de los métodos automáticos: simp, simp_all,
auto, blast, force, fast, arith o metis.
(2) Se pueden establecer lemas auxiliares si se consideran útilies,
siempre que su demostración se realice de forma detallada, sin
usarlos métodos automáticos.
›

end
</source>

← Revisión anterior	Revisión del 09:53 4 may 2020
(Sin diferencias)

T1 - Historial de revisiones

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

Mjoseh: Página creada con « text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)› theory Tarea1 imports Main begin text ‹ Apellidos: Nombre: ›…»