Lógica matemática y fundamentos (2012-13) - Contribuciones del usuario [es]

Lógica matemática y fundamentos

2014-03-05T08:39:21Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]]).

Lógica matemática y fundamentos

2014-03-05T08:17:28Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).

Ejercicio 5

2013-06-10T11:22:38Z

Mjoseh:

== Enunciado ==
El quinto ejercicio evaluable consiste en realizar dos casos de estudio, las expresiones booleanas y las expresiones condicionales. Concretamente:

* Especificación en Haskell de las expresiones booleanaas y de las expresiones condicionales. Funciones que transforman una expresión booleana en una expresión condicional normalizada.

* Demostración de la corrección de la función de transformación, usando Isabelle/HOL.

Los ficheros correspondientes son: ([[Media: Expresiones_If_p.hs |Enunciado en Haskell]] y [[Media: Expresiones_If_p.thy |Enunciado en Isabelle/HOL]]).

Los ficheros con las soluciones (usuario_5.hs y usuario_5.thy) se enviarán a mjoseh@us.es antes del lunes 17 de junio.

Ejercicio 5

2013-06-06T07:45:53Z

Mjoseh:

Archivo:Expresiones If p.thy

2013-06-05T08:02:33Z

Mjoseh:

Archivo:Expresiones If p.hs

2013-06-05T08:02:15Z

Mjoseh:

Ejercicio 5

2013-06-05T08:01:32Z

Mjoseh: Página creada con '== Enunciado == El quinto ejercicio evaluable consiste en realizar dos casos de estudio, las expresiones booleanas y las expresiones condicionales. Concretamente: * Especificac...'

Lógica matemática y fundamentos

2013-06-05T07:48:04Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).
* '''Relación 13''': Programación funcional en Isabelle/HOL. ([[Media:R13.thy |Enunciado]] y [[Relación 13 |Solución colaborativa]]).
* '''Relación 14''': Razonamiento sobre programas con Isabelle/HOL. ([[Media:R14.thy |Enunciado]] y [[Relación 14 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]] ([[Media:T14.thy |Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]] ([[Media:T15.thy |Teoría]]).

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].
* '''Ejercicio 5 (opcional)''': [[Ejercicio 5 | Formas normales condicionales (Haskell e Isabelle/HOL)]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Relación 14

2013-05-29T09:32:35Z

Mjoseh: Página creada con '<source lang = "Isar"> header {* R14: Razonamiento sobre programas en Isabelle/HOL *} theory R14 imports Main begin text {* ------------------------------------------------...'

<source lang = "Isar">
header {* R14: Razonamiento sobre programas en Isabelle/HOL *}

theory R14
imports Main
begin

text {* ---------------------------------------------------------------
Ejercicio 1. Definir la función
sumaImpares :: nat ⇒ nat
tal que (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 5 = 25
------------------------------------------------------------------ *}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares n = undefined"

value "sumaImpares 5" -- "= 25"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
sumaImpares n = n*n
------------------------------------------------------------------- *}

lemma "sumaImpares n = n*n"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
sumaPotenciasDeDosMasUno :: nat ⇒ nat
tal que
(sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.
Por ejemplo,
sumaPotenciasDeDosMasUno 3 = 16
------------------------------------------------------------------ *}

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno n = undefined"

value "sumaPotenciasDeDosMasUno 3" -- "= 16"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
oops

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
copia :: nat ⇒ 'a ⇒ 'a list
tal que (copia n x) es la lista formado por n copias del elemento
x. Por ejemplo,
copia 3 x = [x,x,x]
------------------------------------------------------------------ *}

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia n x = undefined"

value "copia 3 x" -- "= [x,x,x]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de xs cumplen
la propiedad p. Por ejemplo,
todos (λx. x>(1::nat)) [2,6,4] = True
todos (λx. x>(2::nat)) [2,6,4] = False
Nota: La conjunción se representa por ∧
----------------------------------------------------------------- *}

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p xs = undefined"

value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"
value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar que todos los elementos de (copia n x) son
iguales a x.
------------------------------------------------------------------- *}

lemma "todos (λy. y=x) (copia n x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ *}

fun factR :: "nat ⇒ nat" where
"factR n = undefined"

value "factR 4" -- "= 24"

text {* ---------------------------------------------------------------
Ejercicio 9. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
------------------------------------------------------------------- *}

fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (Suc n)*x"

fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"

value "factI 4" -- "= 24"

lemma fact: "factI' n x = x * factR n"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
factI n = factR n
------------------------------------------------------------------- *}

corollary "factI n = factR n"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Definir, recursivamente y sin usar (@), la función
amplia :: 'a list ⇒ 'a ⇒ 'a list
tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
final de la lista xs. Por ejemplo,
amplia [d,a] t = [d,a,t]
------------------------------------------------------------------ *}

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia xs y = undefined"

value "amplia [d,a] t" -- "= [d,a,t]"

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

lemma "amplia xs y = xs @ [y]"
oops

end

</source>

Archivo:R14.thy

2013-05-29T09:31:44Z

Mjoseh:

Lógica matemática y fundamentos

2013-05-29T09:31:14Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).
* '''Relación 13''': Programación funcional en Isabelle/HOL. ([[Media:R13.thy |Enunciado]] y [[Relación 13 |Solución colaborativa]]).
* '''Relación 14''': Razonamiento sobre programas con Isabelle/HOL. ([[Media:R14.thy |Enunciado]] y [[Relación 14 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]] ([[Media:T14.thy |Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]] ([[Media:T15.thy |Teoría]]).

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Tema 15

2013-05-27T07:10:21Z

Mjoseh:

<source lang = "Isar">
header {* Tema 15: Razonamiento sobre programas en Isabelle *}

theory T15
imports Main
begin

text {*
En este tema se demuestra con Isabelle las propiedades de los
programas funcionales como se expone en el tema 8 del curso
"Informática" que puede leerse en
http://www.cs.us.es/~jalonso/cursos/i1m/temas/tema-8t.pdf
*}

section {* Razonamiento ecuacional *}

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: "'a list ⇒ nat" where
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x#xs) = 1 + longitud xs"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

lemma "longitud [4,2,5] = 3"
by simp

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
fun intercambia :: "'a × 'b ⇒ 'b × 'a"
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
"intercambia (2,3) = (3,2)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

value "intercambia (2,3)" -- "= (3,2)"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

lemma "intercambia (intercambia (x,y)) = (x,y)"
by simp

text {* ---------------------------------------------------------------
Ejercicio 5. Definir, por recursión, la función
inversa :: "'a list ⇒ 'a list"
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ [x]"

value "inversa [3,2,5]" -- "= [5,2,3]"

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

lemma "inversa [x] = [x]"
by simp

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
repite :: "nat ⇒ 'a ⇒ 'a list" where
tal que . Por ejemplo,
repite 3 5 = [5,5,5]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
| "repite (Suc n) x = x # (repite n x)"

value "repite 3 5" -- "= [5,5,5]"

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

lemma "longitud (repite n x) = n"
apply (induct_tac n)
apply (auto)
done

lemma "longitud (repite n x) = n"
by (induct n) auto

lemma longitud_repite:
"longitud (repite n x) = n"
proof (induct n)
show "longitud (repite 0 x) = 0" by simp
next
fix n
assume hi: "longitud (repite n x) = n"
show "longitud (repite (Suc n) x) = Suc n"
proof -
have "longitud (repite (Suc n) x) = longitud (x # (repite n x))" by simp
also have "... = 1 + longitud (repite n x)" by simp
also have "... = 1 + n" using hi by simp
also have "... = Suc n" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
fun conc :: "'a list ⇒ 'a list ⇒ 'a list"
tal que . Por ejemplo,
conc [2,3] [4,3,5] = [2,3,4,3,5]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"

value "conc [2,3] [4,3,5]" -- "= [2,3,4,3,5]"

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto

lemma conc_asociativa:
"conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
show "conc [] (conc ys zs) = conc (conc [] ys) zs" by simp
next
fix x xs
assume hi: "conc xs (conc ys zs) = conc (conc xs ys) zs"
show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs"
proof -
have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" by simp
also have "... = x # (conc (conc xs ys) zs)" using hi by simp
also have "... = conc (x#(conc xs ys)) zs" by simp
also have "... = conc (conc (x # xs) ys) zs" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

lemma "conc xs ys = conc ys xs"
quickcheck
oops

text {* Encuentra el contraejemplo,
xs = [a\<^isub>2]
ys = [a\<^isub>1] *}

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

lemma "conc xs [] = xs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto

lemma long_conc:
"longitud (conc xs ys) = longitud xs + longitud ys"
proof (induct xs)
show "longitud (conc [] ys) = longitud [] + longitud ys" by simp
next
fix x xs
assume hi: "longitud (conc xs ys) = longitud xs + longitud ys"
show "longitud (conc (x # xs) ys) = longitud (x # xs) + longitud ys"
proof -
have "longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))" by simp
also have "... = 1 + longitud (conc xs ys)" by simp
also have "... = 1 + (longitud xs + longitud ys)" using hi by simp
also have "... = (1+ longitud xs) + longitud ys" by simp
also have "... = longitud (x # xs) + longitud ys" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 14. Definir la función
coge :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [3,7,5,4] = [3,7]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []"
| "coge 0 xs = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"

value "coge 2 [3,7,5,4]" -- "= [3,7]"

text {* ---------------------------------------------------------------
Ejercicio 15. Definir la función
elimina :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
elimina 2 [3,7,5,4] = [5,4]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

value "elimina 2 [3,7,5,4]" -- "= [5,4]"

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: coge.induct) auto

text {* coge.induct es el esquema de inducción asociado a la definición
de la función coge. Puede verse como sigue: *}

thm coge.induct

lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: elimina.induct) auto

thm elimina.induct

lemma conc_coge_elimina:
"conc (coge n xs) (elimina n xs) = xs"
proof (induct rule: coge.induct)
show "⋀n. conc (coge n []) (elimina n []) = []" by simp
next
show "⋀v va. conc (coge 0 (v # va)) (elimina 0 (v # va)) = v # va" by simp
next
fix x xs n
assume hi: "conc (coge n xs) (elimina n xs) = xs"
show "conc (coge (Suc n) (x # xs)) (elimina (Suc n) (x # xs)) = x # xs"
proof -
have "conc (coge (Suc n) (x # xs)) (elimina (Suc n) (x # xs)) = conc (coge (Suc n) (x # xs)) (elimina n xs)" by simp
also have "... = conc (x# (coge n xs)) (elimina n xs)" by simp
also have "... = x#(conc (coge n xs) (elimina n xs))" by simp
also have "... = (x#xs)" using hi by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Definir la función
esVacia :: "'a list ⇒ bool"
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

lemma "esVacia xs = esVacia (conc xs xs)"
by (induct xs) auto

lemma vacia_conc:
"esVacia xs = esVacia (conc xs xs)"
proof (induct xs)
show "esVacia [] = esVacia (conc [] [])" by simp
next
fix x xs
assume hi: "esVacia xs = esVacia (conc xs xs)"
show "esVacia (x # xs) = esVacia (conc (x # xs) (x # xs))"
proof -
have "esVacia (conc (x # xs) (x # xs)) = esVacia (x# (conc xs (x#xs)))" by simp
also have "... = esVacia (x # xs)" by simp
finally show ?thesis by simp
qed
qed

lemma vacia_conc':
"esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
case Nil thus ?thesis by simp
next
case Cons thus ?thesis by simp
qed

lemma vacia_conc'':
"esVacia xs = esVacia (conc xs xs)"
by (cases xs) simp_all

text {* ---------------------------------------------------------------
Ejercicio 19. Definir la función
inversaAc :: "'a list ⇒ 'a list"
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

value "inversaAc [3,2,5]" -- "= [5,2,3]"

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar que
inversaAcAux xs ys = (inversa xs)@ys
------------------------------------------------------------------- *}

lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

lemma inversaAcAux_es_inversa_b:
"inversaAcAux xs ys = (inversa xs)@ys"
proof (induct xs arbitrary: ys)
show "⋀ys. inversaAcAux [] ys = inversa [] @ ys" by simp
next
fix x xs zs
assume hi: "⋀ys. inversaAcAux xs ys = inversa xs @ ys"
show "inversaAcAux (x#xs) zs = inversa (x#xs) @ zs"
proof -
have "inversaAcAux (x#xs) zs = inversaAcAux xs (x#zs)" by simp
also have "... = inversa xs @ (x#zs)" using hi by simp
also have "... = inversa xs @ [x] @ zs" by simp
also have "... = inversa (x#xs) @ zs" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

text {* ---------------------------------------------------------------
Ejercicio 22. Definir la función
sum :: "int list ⇒ int"
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "int list ⇒ int" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 23. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"

value "map (λx. 2*x) [3::int,2,5]" -- "= [6,4,10]"

value "map (λx. 6*x) [3::int,2,5]" -- "= [18,12,30]"

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto

lemma sum_map:
"sum (map (λx. 2*x) xs) = 2 * (sum xs)"
proof (induct xs)
show "sum (map (λx. 2*x) []) = 2 * (sum [])" by simp
next
fix a xs
assume hi: "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
show "sum (map (λx. 2*x) (a#xs)) = 2 * (sum (a#xs))"
proof -
have "sum (map (λx. 2*x) (a#xs)) = sum ((2*a)#(map (λx. 2*x) xs))" by simp
also have "... = 2*a + sum (map (λx. 2*x) xs)" by simp
also have "... = 2*a + 2 * (sum xs)" using hi by simp
also have "... = 2*(a + sum xs)" by simp
also have "... = 2 * (sum (a#xs))"by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

lemma "longitud (map f xs) = longitud xs"
by (induct xs) auto

lemma long_map:
"longitud (map f xs) = longitud xs"
proof (induct xs)
show "longitud (map f []) = longitud []" by simp
next
fix x xs
assume hi: "longitud (map f xs) = longitud xs"
show "longitud (map f (x#xs)) = longitud (x#xs)"
proof -
have "longitud (map f (x#xs)) = longitud ((f x)#(map f xs))" by simp
also have "... = 1 + longitud (map f xs)" by simp
also have "... = 1 + longitud xs" using hi by simp
also have "... = longitud (x#xs)" by simp
finally show ?thesis .
qed
qed

end
</source>

Archivo:T15.thy

2013-05-27T07:06:52Z

Mjoseh:

Archivo:R13.thy

2013-05-27T07:06:27Z

Mjoseh: subió una nueva versión de «Archivo:R13.thy»

Archivo:R13.thy

2013-05-27T07:06:10Z

Mjoseh:

Archivo:T14.thy

2013-05-22T11:52:53Z

Mjoseh:

Tema 15

2013-05-22T08:21:18Z

Mjoseh: Página blanqueada

Relación 13

2013-05-22T08:20:40Z

Mjoseh: Página creada con '<source lang = "Isar"> header {* R13: Programación funcional en Isabelle *} theory R13 imports Main begin text {* ------------------------------------------------------------...'

<source lang = "Isar">
header {* R13: Programación funcional en Isabelle *}

theory R13
imports Main
begin

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: "'a list ⇒ nat" where
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud xs = undefined"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
fun intercambia :: "'a × 'b ⇒ 'b × 'a"
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
"intercambia (2,3) = (3,2)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = undefined"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: "'a list ⇒ 'a list"
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = undefined"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 4. Definir la función
repite :: "nat ⇒ 'a ⇒ 'a list" where
tal que . Por ejemplo,
repite 3 5 = [5,5,5]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite n x = undefined"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
fun conc :: "'a list ⇒ 'a list ⇒ 'a list"
tal que . Por ejemplo,
conc [2,3] [4,3,5] = [2,3,4,3,5]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc xs ys = undefined"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [3,7,5,4] = [3,7]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n xs = undefined"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
elimina 2 [3,7,5,4] = [5,4]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n xs = undefined"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: "'a list ⇒ bool"
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia xs = undefined"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: "'a list ⇒ 'a list"
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux xs ys = undefined"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = undefined"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 10. Definir la función
sum :: "int list ⇒ int"
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum xs = undefined"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f xs = undefined"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

end
</source>

Lógica matemática y fundamentos

2013-05-22T08:19:50Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).
* '''Relación 13''': Programación funcional en Isabelle/HOL. ([[Media:R13.thy |Enunciado]] y [[Relación 13 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]] ([[Media:T14.thy |Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]] ([[Media:T15.thy |Teoría]]).

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Lógica matemática y fundamentos

2013-05-22T08:13:44Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]] ([[Media:T14.thy |Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]] ([[Media:T15.thy |Teoría]]).

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Tema 15

2013-05-22T08:13:02Z

Mjoseh:

<source lang = "Isar">

header {* Tema 15: Razonamiento sobre programas en Isabelle *}

theory T15
imports Main
begin

text {*
En este tema se demuestra con Isabelle las propiedades de los
programas funcionales como se expone en el tema 8 del curso
"Informática" que puede leerse en
http://www.cs.us.es/~jalonso/cursos/i1m/temas/tema-8t.pdf
*}

section {* Razonamiento ecuacional *}

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: "'a list ⇒ nat" where
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x#xs) = 1 + longitud xs"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

lemma "longitud [4,2,5] = 3"
by simp

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
fun intercambia :: "'a × 'b ⇒ 'b × 'a"
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
"intercambia (2,3) = (3,2)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

value "intercambia (2,3)" -- "= (3,2)"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

lemma "intercambia (intercambia (x,y)) = (x,y)"
by simp

text {* ---------------------------------------------------------------
Ejercicio 5. Definir, por recursión, la función
inversa :: "'a list ⇒ 'a list"
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ [x]"

value "inversa [3,2,5]" -- "= [5,2,3]"

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

lemma "inversa [x] = [x]"
by simp

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
repite :: "nat ⇒ 'a ⇒ 'a list" where
tal que . Por ejemplo,
repite 3 5 = [5,5,5]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
| "repite (Suc n) x = x # (repite n x)"

value "repite 3 5" -- "= [5,5,5]"

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

lemma "longitud (repite n x) = n"
apply (induct_tac n)
apply (auto)
done

lemma "longitud (repite n x) = n"
by (induct n) auto

lemma longitud_repite:
"longitud (repite n x) = n"
proof (induct n)
show "longitud (repite 0 x) = 0" by simp
next
fix n
assume hi: "longitud (repite n x) = n"
show "longitud (repite (Suc n) x) = Suc n"
proof -
have "longitud (repite (Suc n) x) = longitud (x # (repite n x))" by simp
also have "... = 1 + longitud (repite n x)" by simp
also have "... = 1 + n" using hi by simp
also have "... = Suc n" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
fun conc :: "'a list ⇒ 'a list ⇒ 'a list"
tal que . Por ejemplo,
conc [2,3] [4,3,5] = [2,3,4,3,5]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"

value "conc [2,3] [4,3,5]" -- "= [2,3,4,3,5]"

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto

lemma conc_asociativa:
"conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
show "conc [] (conc ys zs) = conc (conc [] ys) zs" by simp
next
fix x xs
assume hi: "conc xs (conc ys zs) = conc (conc xs ys) zs"
show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs"
proof -
have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" by simp
also have "... = x # (conc (conc xs ys) zs)" using hi by simp
also have "... = conc (x#(conc xs ys)) zs" by simp
also have "... = conc (conc (x # xs) ys) zs" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

lemma "conc xs ys = conc ys xs"
quickcheck
oops

text {* Encuentra el contraejemplo,
xs = [a\<^isub>2]
ys = [a\<^isub>1] *}

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

lemma "conc xs [] = xs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto

lemma long_conc:
"longitud (conc xs ys) = longitud xs + longitud ys"
proof (induct xs)
show "longitud (conc [] ys) = longitud [] + longitud ys" by simp
next
fix x xs
assume hi: "longitud (conc xs ys) = longitud xs + longitud ys"
show "longitud (conc (x # xs) ys) = longitud (x # xs) + longitud ys"
proof -
have "longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))" by simp
also have "... = 1 + longitud (conc xs ys)" by simp
also have "... = 1 + (longitud xs + longitud ys)" using hi by simp
also have "... = (1+ longitud xs) + longitud ys" by simp
also have "... = longitud (x # xs) + longitud ys" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 14. Definir la función
coge :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [3,7,5,4] = [3,7]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []"
| "coge 0 xs = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"

value "coge 2 [3,7,5,4]" -- "= [3,7]"

text {* ---------------------------------------------------------------
Ejercicio 15. Definir la función
elimina :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
elimina 2 [3,7,5,4] = [5,4]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

value "elimina 2 [3,7,5,4]" -- "= [5,4]"

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: coge.induct) auto

text {* coge.induct es el esquema de inducción asociado a la definición
de la función coge. Puede verse como sigue: *}

thm coge.induct

lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: elimina.induct) auto

thm elimina.induct

lemma conc_coge_elimina:
"conc (coge n xs) (elimina n xs) = xs"
proof (induct rule: coge.induct)
show "⋀n. conc (coge n []) (elimina n []) = []" by simp
next
show "⋀v va. conc (coge 0 (v # va)) (elimina 0 (v # va)) = v # va" by simp
next
fix x xs n
assume hi: "conc (coge n xs) (elimina n xs) = xs"
show "conc (coge (Suc n) (x # xs)) (elimina (Suc n) (x # xs)) = x # xs"
proof -
have "conc (coge (Suc n) (x # xs)) (elimina (Suc n) (x # xs)) = conc (coge (Suc n) (x # xs)) (elimina n xs)" by simp
also have "... = conc (x# (coge n xs)) (elimina n xs)" by simp
also have "... = x#(conc (coge n xs) (elimina n xs))" by simp
also have "... = (x#xs)" using hi by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Definir la función
esVacia :: "'a list ⇒ bool"
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

lemma "esVacia xs = esVacia (conc xs xs)"
by (induct xs) auto

lemma vacia_conc:
"esVacia xs = esVacia (conc xs xs)"
proof (induct xs)
show "esVacia [] = esVacia (conc [] [])" by simp
next
fix x xs
assume hi: "esVacia xs = esVacia (conc xs xs)"
show "esVacia (x # xs) = esVacia (conc (x # xs) (x # xs))"
proof -
have "esVacia (conc (x # xs) (x # xs)) = esVacia (x# (conc xs (x#xs)))" by simp
also have "... = esVacia (x # xs)" by simp
finally show ?thesis by simp
qed
qed

lemma vacia_conc':
"esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
case Nil thus ?thesis by simp
next
case Cons thus ?thesis by simp
qed

lemma vacia_conc'':
"esVacia xs = esVacia (conc xs xs)"
by (cases xs) simp_all

text {* ---------------------------------------------------------------
Ejercicio 19. Definir la función
inversaAc :: "'a list ⇒ 'a list"
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

value "inversaAc [3,2,5]" -- "= [5,2,3]"

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar que
inversaAcAux xs ys = (inversa xs)@ys
------------------------------------------------------------------- *}

lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

lemma inversaAcAux_es_inversa_b:
"inversaAcAux xs ys = (inversa xs)@ys"
proof (induct xs arbitrary: ys)
show "⋀ys. inversaAcAux [] ys = inversa [] @ ys" by simp
next
fix x xs zs
assume hi: "⋀ys. inversaAcAux xs ys = inversa xs @ ys"
show "inversaAcAux (x#xs) zs = inversa (x#xs) @ zs"
proof -
have "inversaAcAux (x#xs) zs = inversaAcAux xs (x#zs)" by simp
also have "... = inversa xs @ (x#zs)" using hi by simp
also have "... = inversa xs @ [x] @ zs" by simp
also have "... = inversa (x#xs) @ zs" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

text {* ---------------------------------------------------------------
Ejercicio 22. Definir la función
sum :: "int list ⇒ int"
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "int list ⇒ int" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 23. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"

value "map (λx. 2*x) [3::int,2,5]" -- "= [6,4,10]"

value "map (λx. 6*x) [3::int,2,5]" -- "= [18,12,30]"

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto

lemma sum_map:
"sum (map (λx. 2*x) xs) = 2 * (sum xs)"
proof (induct xs)
show "sum (map (λx. 2*x) []) = 2 * (sum [])" by simp
next
fix a xs
assume hi: "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
show "sum (map (λx. 2*x) (a#xs)) = 2 * (sum (a#xs))"
proof -
have "sum (map (λx. 2*x) (a#xs)) = sum ((2*a)#(map (λx. 2*x) xs))" by simp
also have "... = 2*a + sum (map (λx. 2*x) xs)" by simp
also have "... = 2*a + 2 * (sum xs)" using hi by simp
also have "... = 2*(a + sum xs)" by simp
also have "... = 2 * (sum (a#xs))"by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

lemma "longitud (map f xs) = longitud xs"
by (induct xs) auto

lemma long_map:
"longitud (map f xs) = longitud xs"
proof (induct xs)
show "longitud (map f []) = longitud []" by simp
next
fix x xs
assume hi: "longitud (map f xs) = longitud xs"
show "longitud (map f (x#xs)) = longitud (x#xs)"
proof -
have "longitud (map f (x#xs)) = longitud ((f x)#(map f xs))" by simp
also have "... = 1 + longitud (map f xs)" by simp
also have "... = 1 + longitud xs" using hi by simp
also have "... = longitud (x#xs)" by simp
finally show ?thesis .
qed
qed

end
</source>

Tema 15

2013-05-22T08:12:34Z

Mjoseh: Página creada con '<source lang = Isar"> header {* Tema 15: Razonamiento sobre programas en Isabelle *} theory T15 imports Main begin text {* En este tema se demuestra con Isabelle las propie...'

<source lang = Isar">
header {* Tema 15: Razonamiento sobre programas en Isabelle *}

theory T15
imports Main
begin

text {*
En este tema se demuestra con Isabelle las propiedades de los
programas funcionales como se expone en el tema 8 del curso
"Informática" que puede leerse en
http://www.cs.us.es/~jalonso/cursos/i1m/temas/tema-8t.pdf
*}

section {* Razonamiento ecuacional *}

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: "'a list ⇒ nat" where
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x#xs) = 1 + longitud xs"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

lemma "longitud [4,2,5] = 3"
by simp

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
fun intercambia :: "'a × 'b ⇒ 'b × 'a"
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
"intercambia (2,3) = (3,2)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

value "intercambia (2,3)" -- "= (3,2)"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

lemma "intercambia (intercambia (x,y)) = (x,y)"
by simp

text {* ---------------------------------------------------------------
Ejercicio 5. Definir, por recursión, la función
inversa :: "'a list ⇒ 'a list"
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ [x]"

value "inversa [3,2,5]" -- "= [5,2,3]"

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

lemma "inversa [x] = [x]"
by simp

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
repite :: "nat ⇒ 'a ⇒ 'a list" where
tal que . Por ejemplo,
repite 3 5 = [5,5,5]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
| "repite (Suc n) x = x # (repite n x)"

value "repite 3 5" -- "= [5,5,5]"

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

lemma "longitud (repite n x) = n"
apply (induct_tac n)
apply (auto)
done

lemma "longitud (repite n x) = n"
by (induct n) auto

lemma longitud_repite:
"longitud (repite n x) = n"
proof (induct n)
show "longitud (repite 0 x) = 0" by simp
next
fix n
assume hi: "longitud (repite n x) = n"
show "longitud (repite (Suc n) x) = Suc n"
proof -
have "longitud (repite (Suc n) x) = longitud (x # (repite n x))" by simp
also have "... = 1 + longitud (repite n x)" by simp
also have "... = 1 + n" using hi by simp
also have "... = Suc n" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
fun conc :: "'a list ⇒ 'a list ⇒ 'a list"
tal que . Por ejemplo,
conc [2,3] [4,3,5] = [2,3,4,3,5]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"

value "conc [2,3] [4,3,5]" -- "= [2,3,4,3,5]"

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto

lemma conc_asociativa:
"conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
show "conc [] (conc ys zs) = conc (conc [] ys) zs" by simp
next
fix x xs
assume hi: "conc xs (conc ys zs) = conc (conc xs ys) zs"
show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs"
proof -
have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" by simp
also have "... = x # (conc (conc xs ys) zs)" using hi by simp
also have "... = conc (x#(conc xs ys)) zs" by simp
also have "... = conc (conc (x # xs) ys) zs" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

lemma "conc xs ys = conc ys xs"
quickcheck
oops

text {* Encuentra el contraejemplo,
xs = [a\<^isub>2]
ys = [a\<^isub>1] *}

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

lemma "conc xs [] = xs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto

lemma long_conc:
"longitud (conc xs ys) = longitud xs + longitud ys"
proof (induct xs)
show "longitud (conc [] ys) = longitud [] + longitud ys" by simp
next
fix x xs
assume hi: "longitud (conc xs ys) = longitud xs + longitud ys"
show "longitud (conc (x # xs) ys) = longitud (x # xs) + longitud ys"
proof -
have "longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))" by simp
also have "... = 1 + longitud (conc xs ys)" by simp
also have "... = 1 + (longitud xs + longitud ys)" using hi by simp
also have "... = (1+ longitud xs) + longitud ys" by simp
also have "... = longitud (x # xs) + longitud ys" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 14. Definir la función
coge :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [3,7,5,4] = [3,7]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []"
| "coge 0 xs = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"

value "coge 2 [3,7,5,4]" -- "= [3,7]"

text {* ---------------------------------------------------------------
Ejercicio 15. Definir la función
elimina :: "nat ⇒ 'a list ⇒ 'a list"
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
elimina 2 [3,7,5,4] = [5,4]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

value "elimina 2 [3,7,5,4]" -- "= [5,4]"

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: coge.induct) auto

text {* coge.induct es el esquema de inducción asociado a la definición
de la función coge. Puede verse como sigue: *}

thm coge.induct

lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: elimina.induct) auto

thm elimina.induct

lemma conc_coge_elimina:
"conc (coge n xs) (elimina n xs) = xs"
proof (induct rule: coge.induct)
show "⋀n. conc (coge n []) (elimina n []) = []" by simp
next
show "⋀v va. conc (coge 0 (v # va)) (elimina 0 (v # va)) = v # va" by simp
next
fix x xs n
assume hi: "conc (coge n xs) (elimina n xs) = xs"
show "conc (coge (Suc n) (x # xs)) (elimina (Suc n) (x # xs)) = x # xs"
proof -
have "conc (coge (Suc n) (x # xs)) (elimina (Suc n) (x # xs)) = conc (coge (Suc n) (x # xs)) (elimina n xs)" by simp
also have "... = conc (x# (coge n xs)) (elimina n xs)" by simp
also have "... = x#(conc (coge n xs) (elimina n xs))" by simp
also have "... = (x#xs)" using hi by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Definir la función
esVacia :: "'a list ⇒ bool"
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

lemma "esVacia xs = esVacia (conc xs xs)"
by (induct xs) auto

lemma vacia_conc:
"esVacia xs = esVacia (conc xs xs)"
proof (induct xs)
show "esVacia [] = esVacia (conc [] [])" by simp
next
fix x xs
assume hi: "esVacia xs = esVacia (conc xs xs)"
show "esVacia (x # xs) = esVacia (conc (x # xs) (x # xs))"
proof -
have "esVacia (conc (x # xs) (x # xs)) = esVacia (x# (conc xs (x#xs)))" by simp
also have "... = esVacia (x # xs)" by simp
finally show ?thesis by simp
qed
qed

lemma vacia_conc':
"esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
case Nil thus ?thesis by simp
next
case Cons thus ?thesis by simp
qed

lemma vacia_conc'':
"esVacia xs = esVacia (conc xs xs)"
by (cases xs) simp_all

text {* ---------------------------------------------------------------
Ejercicio 19. Definir la función
inversaAc :: "'a list ⇒ 'a list"
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [3,2,5] = [5,2,3]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

value "inversaAc [3,2,5]" -- "= [5,2,3]"

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar que
inversaAcAux xs ys = (inversa xs)@ys
------------------------------------------------------------------- *}

lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

lemma inversaAcAux_es_inversa_b:
"inversaAcAux xs ys = (inversa xs)@ys"
proof (induct xs arbitrary: ys)
show "⋀ys. inversaAcAux [] ys = inversa [] @ ys" by simp
next
fix x xs zs
assume hi: "⋀ys. inversaAcAux xs ys = inversa xs @ ys"
show "inversaAcAux (x#xs) zs = inversa (x#xs) @ zs"
proof -
have "inversaAcAux (x#xs) zs = inversaAcAux xs (x#zs)" by simp
also have "... = inversa xs @ (x#zs)" using hi by simp
also have "... = inversa xs @ [x] @ zs" by simp
also have "... = inversa (x#xs) @ zs" by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

text {* ---------------------------------------------------------------
Ejercicio 22. Definir la función
sum :: "int list ⇒ int"
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "int list ⇒ int" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 23. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"

value "map (λx. 2*x) [3::int,2,5]" -- "= [6,4,10]"

value "map (λx. 6*x) [3::int,2,5]" -- "= [18,12,30]"

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto

lemma sum_map:
"sum (map (λx. 2*x) xs) = 2 * (sum xs)"
proof (induct xs)
show "sum (map (λx. 2*x) []) = 2 * (sum [])" by simp
next
fix a xs
assume hi: "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
show "sum (map (λx. 2*x) (a#xs)) = 2 * (sum (a#xs))"
proof -
have "sum (map (λx. 2*x) (a#xs)) = sum ((2*a)#(map (λx. 2*x) xs))" by simp
also have "... = 2*a + sum (map (λx. 2*x) xs)" by simp
also have "... = 2*a + 2 * (sum xs)" using hi by simp
also have "... = 2*(a + sum xs)" by simp
also have "... = 2 * (sum (a#xs))"by simp
finally show ?thesis .
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

lemma "longitud (map f xs) = longitud xs"
by (induct xs) auto

lemma long_map:
"longitud (map f xs) = longitud xs"
proof (induct xs)
show "longitud (map f []) = longitud []" by simp
next
fix x xs
assume hi: "longitud (map f xs) = longitud xs"
show "longitud (map f (x#xs)) = longitud (x#xs)"
proof -
have "longitud (map f (x#xs)) = longitud ((f x)#(map f xs))" by simp
also have "... = 1 + longitud (map f xs)" by simp
also have "... = 1 + longitud xs" using hi by simp
also have "... = longitud (x#xs)" by simp
finally show ?thesis .
qed
qed

end
</source>

Lógica matemática y fundamentos

2013-05-22T08:11:50Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).

=== Teorías Isabelle/HOL de los temas de deducción natural ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]] ([[Media:T14.thy |Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]] ([[Media:T15.thy |Teoría]]).

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Lógica matemática y fundamentos

2013-05-22T08:11:28Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).

=== Teorías Isabelle/HOL de los temas de deducción natural ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]] ([[Media:T14.thy |Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]]([[Media:T15.thy |Teoría]]).

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Tema 14

2013-05-22T08:10:50Z

Mjoseh:

<source lang = "Isar">

header {* Tema 14: Programación funcional en Isabelle *}

theory T14
imports Main
begin

section {* Introducción *}

text {*
En este tema se presenta el lenguaje funcional que está
incluido en Isabelle. El lenguaje funcional es muy parecido a
Haskell. *}

section {* Números naturales, enteros y booleanos *}

text {* En Isabelle están definidos los número naturales con la sintaxis
de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).

Los números como el 1 son abreviaturas de los correspondientes en la
notación de Peano, en este caso "Suc 0".

El tipo de los números naturales es nat.

Por ejemplo, el siguiente del 0 es el 1. *}

value "Suc 0" -- "= 1"

text {* En Isabelle está definida la suma de los números naturales:
(x + y) es la suma de x e y.

Por ejemplo, la suma de los números naturales 1 y 2 es el número
natural 3. *}

value "(1::nat) + 2" -- "= 3"

text {* La notación del par de dos puntos se usa para asignar un tipo a
un término (por ejemplo, (1::nat) significa que se considera que 1 es
un número natural).

En Isabelle está definida el producto de los números naturales:
(x * y) es el producto de x e y.

Por ejemplo, el producto de los números naturales 2 y 3 es el número
natural 6. *}

value "(2::nat) * 3" -- "= 6"

text {* En Isabelle está definida la división de números naturales:
(n div m) es el cociente entero de x entre y.

Por ejemplo, la división natural de 7 entre 3 es 2. *}

value "(7::nat) div 3" -- "= 2"

text {* En Isabelle está definida el resto de división de números
naturales: (n mod m) es el resto de dividir n entre m.

Por ejemplo, el resto de dividir 7 entre 3 es 1. *}

value "(7::nat) mod 3" -- "= 1"

text {* En Isabelle también están definidos los números enteros. El tipo
de los enteros se representa por int.

Por ejemplo, la suma de 1 y -2 es el número entero -1. *}

value "(1::int) + -2" -- "= -1"

text {* Los numerales están sobrecargados. Por ejemplo, el 1 puede ser
un natural o un entero, dependiendo del contexto.

Isabelle resuelve ambigüedades mediante inferencia de tipos.

A veces, es necesario usar declaraciones de tipo para resolver la
ambigüedad.

En Isabelle están definidos los valores booleanos (True y False), las
conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃).

El tipo de los booleanos es bool. *}

text {* La conjunción de dos fórmulas verdaderas es verdadera. *}
value "True ∧ True" -- "= True"

text {* La conjunción de un fórmula verdadera y una falsa es falsa. *}
value "True ∧ False" -- "= False"

text {* La disyunción de una fórmula verdadera y una falsa es
verdadera. *}
value "True ∨ False" -- "= True"

text {* La disyunción de dos fórmulas falsas es falsa. *}
value "False ∨ False" -- "= False"

text {* La negación de una fórmula verdadera es falsa. *}
value "¬True" -- "= False"

text {* Una fórmula falsa implica una fórmula verdadera. *}
value "False ⟶ True" -- "= True"

text {* Un lema introduce una proposición seguida de una demostración.

Isabelle dispone de varios procedimientos automáticos para generar
demostraciones, uno de los cuales es el de simplificación (llamado
simp).

El procedimiento simp aplica un conjunto de reglas de reescritura, que
inicialmente contiene un gran número de reglas relativas a los objetos
definidos. *}

text {* Ej. de simp: Todo elemento es igual a sí mismo. *}
lemma "∀x. x = x"
by simp

text {* Ej. de simp: Existe un elemento igual a 1. *}
lemma "∃x. x = 1"
by simp

section {* Definiciones no recursivas *}

text {* La disyunción exclusiva de A y B se verifica si una es verdadera
y la otra no lo es. *}

definition xor :: "bool ⇒ bool ⇒ bool" where
"xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"

text {* Prop.: La disyunción exclusiva de dos fórmulas verdaderas es
falsa.

Dem.: Por simplificación, usando la definición de la disyunción
exclusiva.
*}

lemma "xor True True = False"
by (simp add: xor_def)

text {* Se añade la definición de la disyunción exclusiva al conjunto de
reglas de simplificación automáticas. *}

declare xor_def[simp]

lemma "xor True False = True"
by simp

section {* Definiciones locales *}

text {* Se puede asignar valores a variables locales mediante 'let' y
usarlo en las expresiones dentro de 'in'.

Por ejemplo, si x es el número natural 3, entonces "x*x=9". *}

value "let x = 3::nat in x * x" -- "= 9"

section {* Pares *}

text {* Un par se representa escribiendo los elementos entre paréntesis
y separados por coma.

El tipo de los pares es el producto de los tipos.

La función fst devuelve el primer elemento de un par y la snd el
segundo.

Por ejemplo, si p es el par de números naturales (2,3), entonces la
suma del primer elemento de p y 1 es igual al segundo elemento de
p. *}

value "let p = (2,3)::nat × nat in fst p + 1 = snd p"

section {* Listas *}

text {* Una lista se representa escribiendo los elementos entre
corchetes y separados por comas.

La lista vacía se representa por [].

Todos los elementos de una lista tienen que ser del mismo tipo.

El tipo de las listas de elementos del tipo a es (a list).

El término (x#xs) representa la lista obtenida añadiendo el elemento x
al principio de la lista xs.

Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista
vacía los elementos c, b y a es [a,b,c]. *}

value "a#(b#(c#[]))" -- "= [a,b,c]"

text {* Funciones de descomposión de listas:
· (hd xs) es el primer elemento de la lista xs.
· (tl xs) es el resto de la lista xs.

Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a
y el resto de xs es [b,c]. *}

value "let xs = [a,b,c] in hd xs = a ∧ tl xs = [b,c]" -- "= True"

text {* (length xs) es la longitud de la lista xs. Por ejemplo, la
longitud de la lista [1,2,3] es 3. *}

value "length [1,2,3]" -- "= 3"

text {* En la sesión 47 de "Isabelle/HOL — Higher-Order Logic"
http://goo.gl/sFsFF se encuentran más definiciones y propiedades de
las listas. *}

section {* Registros *}

text {* Un registro es una colección de campos y valores.

Por ejemplo, los puntos del plano se pueden representar mediante
registros con dos campos, las coordenadas, con valores enteros. *}

record punto =
coordenada_x :: int
coordenada_y :: int

text {* Ejemplo, el punto pt tiene de coordenadas 3 y 7. *}

definition pt :: punto where
"pt ≡ (|coordenada_x = 3, coordenada_y = 7|)"

text {* Ejemplo, la coordenada x del punto pt es 3. *}

value "coordenada_x pt" -- "= 3"

text {* Ejemplo, sea pt2 el punto obtenido a partir del punto pt
cambiando el valor de su coordenada x por 4. Entonces la coordenada x
del punto pt2 es 4. *}

value "let pt2 = pt(|coordenada_x:=4|) in coordenada_x (pt2)" -- "= 4"

section {* Funciones anónimas *}

text {* En Isabelle pueden definirse funciones anónimas.

Por ejemplo, el valor de la función que a un número le asigna su doble
aplicada a 1 es 2. *}

value "(λx. x + x) 1::nat" -- "= 2"

section {* Condicionales *}

text {* El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso
contrario. *}

definition absoluto :: "int ⇒ int" where
"absoluto x ≡ (if x ≥ 0 then x else -x)"

text {* Ejemplo, el valor absoluto de -3 es 3. *}

value "absoluto(-3)" -- "= 3"

text {* Def.: Un número natural n es un sucesor si es de la forma
(Suc m). *}

definition es_sucesor :: "nat ⇒ bool" where
"es_sucesor n ≡ (case n of
0 ⇒ False
| Suc m ⇒ True)"

text {* Ejemplo, el número 3 es sucesor. *}

value "es_sucesor 3" -- "= True"

section {* Tipos de datos y definiciones recursivas *}

text {* Una lista de elementos de tipo a es la lista Vacia o se obtiene
añadiendo, con Cons, un elemento de tipo a a una lista de elementos de
tipo a. *}

datatype 'a Lista = Vacia | Cons 'a "'a Lista"

text {* (conc xs ys) es la concatenación de las lista xs e ys. Por
ejemplo,
conc (Cons a (Cons b Vacia)) (Cons c Vacia)
= Cons a (Cons b (Cons c Vacia))
*}

fun conc :: "'a Lista ⇒ 'a Lista ⇒ 'a Lista" where
"conc Vacia ys = ys"
| "conc (Cons x xs) ys = Cons x (conc xs ys)"

value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
-- "= Cons a (Cons b (Cons c Vacia))"

text {* (suma n) es la suma de los primeros n números naturales. Por
ejemplo,
suma 3 = 6
*}

fun suma :: "nat ⇒ nat" where
"suma 0 = 0"
| "suma (Suc m) = (Suc m) + suma m"

value "suma 3" -- "= 6"

text {* (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 3 = 9
*}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n"

value "sumaImpares 3" -- "= 9"

end

</source>

Tema 14

2013-05-22T08:09:59Z

Mjoseh:

<source lang = "haskell">

header {* Tema 14: Programación funcional en Isabelle *}

theory T14
imports Main
begin

section {* Introducción *}

text {*
En este tema se presenta el lenguaje funcional que está
incluido en Isabelle. El lenguaje funcional es muy parecido a
Haskell. *}

section {* Números naturales, enteros y booleanos *}

text {* En Isabelle están definidos los número naturales con la sintaxis
de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).

Los números como el 1 son abreviaturas de los correspondientes en la
notación de Peano, en este caso "Suc 0".

El tipo de los números naturales es nat.

Por ejemplo, el siguiente del 0 es el 1. *}

value "Suc 0" -- "= 1"

text {* En Isabelle está definida la suma de los números naturales:
(x + y) es la suma de x e y.

Por ejemplo, la suma de los números naturales 1 y 2 es el número
natural 3. *}

value "(1::nat) + 2" -- "= 3"

text {* La notación del par de dos puntos se usa para asignar un tipo a
un término (por ejemplo, (1::nat) significa que se considera que 1 es
un número natural).

En Isabelle está definida el producto de los números naturales:
(x * y) es el producto de x e y.

Por ejemplo, el producto de los números naturales 2 y 3 es el número
natural 6. *}

value "(2::nat) * 3" -- "= 6"

text {* En Isabelle está definida la división de números naturales:
(n div m) es el cociente entero de x entre y.

Por ejemplo, la división natural de 7 entre 3 es 2. *}

value "(7::nat) div 3" -- "= 2"

text {* En Isabelle está definida el resto de división de números
naturales: (n mod m) es el resto de dividir n entre m.

Por ejemplo, el resto de dividir 7 entre 3 es 1. *}

value "(7::nat) mod 3" -- "= 1"

text {* En Isabelle también están definidos los números enteros. El tipo
de los enteros se representa por int.

Por ejemplo, la suma de 1 y -2 es el número entero -1. *}

value "(1::int) + -2" -- "= -1"

text {* Los numerales están sobrecargados. Por ejemplo, el 1 puede ser
un natural o un entero, dependiendo del contexto.

Isabelle resuelve ambigüedades mediante inferencia de tipos.

A veces, es necesario usar declaraciones de tipo para resolver la
ambigüedad.

En Isabelle están definidos los valores booleanos (True y False), las
conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃).

El tipo de los booleanos es bool. *}

text {* La conjunción de dos fórmulas verdaderas es verdadera. *}
value "True ∧ True" -- "= True"

text {* La conjunción de un fórmula verdadera y una falsa es falsa. *}
value "True ∧ False" -- "= False"

text {* La disyunción de una fórmula verdadera y una falsa es
verdadera. *}
value "True ∨ False" -- "= True"

text {* La disyunción de dos fórmulas falsas es falsa. *}
value "False ∨ False" -- "= False"

text {* La negación de una fórmula verdadera es falsa. *}
value "¬True" -- "= False"

text {* Una fórmula falsa implica una fórmula verdadera. *}
value "False ⟶ True" -- "= True"

text {* Un lema introduce una proposición seguida de una demostración.

Isabelle dispone de varios procedimientos automáticos para generar
demostraciones, uno de los cuales es el de simplificación (llamado
simp).

El procedimiento simp aplica un conjunto de reglas de reescritura, que
inicialmente contiene un gran número de reglas relativas a los objetos
definidos. *}

text {* Ej. de simp: Todo elemento es igual a sí mismo. *}
lemma "∀x. x = x"
by simp

text {* Ej. de simp: Existe un elemento igual a 1. *}
lemma "∃x. x = 1"
by simp

section {* Definiciones no recursivas *}

text {* La disyunción exclusiva de A y B se verifica si una es verdadera
y la otra no lo es. *}

definition xor :: "bool ⇒ bool ⇒ bool" where
"xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"

text {* Prop.: La disyunción exclusiva de dos fórmulas verdaderas es
falsa.

Dem.: Por simplificación, usando la definición de la disyunción
exclusiva.
*}

lemma "xor True True = False"
by (simp add: xor_def)

text {* Se añade la definición de la disyunción exclusiva al conjunto de
reglas de simplificación automáticas. *}

declare xor_def[simp]

lemma "xor True False = True"
by simp

section {* Definiciones locales *}

text {* Se puede asignar valores a variables locales mediante 'let' y
usarlo en las expresiones dentro de 'in'.

Por ejemplo, si x es el número natural 3, entonces "x*x=9". *}

value "let x = 3::nat in x * x" -- "= 9"

section {* Pares *}

text {* Un par se representa escribiendo los elementos entre paréntesis
y separados por coma.

El tipo de los pares es el producto de los tipos.

La función fst devuelve el primer elemento de un par y la snd el
segundo.

Por ejemplo, si p es el par de números naturales (2,3), entonces la
suma del primer elemento de p y 1 es igual al segundo elemento de
p. *}

value "let p = (2,3)::nat × nat in fst p + 1 = snd p"

section {* Listas *}

text {* Una lista se representa escribiendo los elementos entre
corchetes y separados por comas.

La lista vacía se representa por [].

Todos los elementos de una lista tienen que ser del mismo tipo.

El tipo de las listas de elementos del tipo a es (a list).

El término (x#xs) representa la lista obtenida añadiendo el elemento x
al principio de la lista xs.

Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista
vacía los elementos c, b y a es [a,b,c]. *}

value "a#(b#(c#[]))" -- "= [a,b,c]"

text {* Funciones de descomposión de listas:
· (hd xs) es el primer elemento de la lista xs.
· (tl xs) es el resto de la lista xs.

Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a
y el resto de xs es [b,c]. *}

value "let xs = [a,b,c] in hd xs = a ∧ tl xs = [b,c]" -- "= True"

text {* (length xs) es la longitud de la lista xs. Por ejemplo, la
longitud de la lista [1,2,3] es 3. *}

value "length [1,2,3]" -- "= 3"

text {* En la sesión 47 de "Isabelle/HOL — Higher-Order Logic"
http://goo.gl/sFsFF se encuentran más definiciones y propiedades de
las listas. *}

section {* Registros *}

text {* Un registro es una colección de campos y valores.

Por ejemplo, los puntos del plano se pueden representar mediante
registros con dos campos, las coordenadas, con valores enteros. *}

record punto =
coordenada_x :: int
coordenada_y :: int

text {* Ejemplo, el punto pt tiene de coordenadas 3 y 7. *}

definition pt :: punto where
"pt ≡ (|coordenada_x = 3, coordenada_y = 7|)"

text {* Ejemplo, la coordenada x del punto pt es 3. *}

value "coordenada_x pt" -- "= 3"

text {* Ejemplo, sea pt2 el punto obtenido a partir del punto pt
cambiando el valor de su coordenada x por 4. Entonces la coordenada x
del punto pt2 es 4. *}

value "let pt2 = pt(|coordenada_x:=4|) in coordenada_x (pt2)" -- "= 4"

section {* Funciones anónimas *}

text {* En Isabelle pueden definirse funciones anónimas.

Por ejemplo, el valor de la función que a un número le asigna su doble
aplicada a 1 es 2. *}

value "(λx. x + x) 1::nat" -- "= 2"

section {* Condicionales *}

text {* El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso
contrario. *}

definition absoluto :: "int ⇒ int" where
"absoluto x ≡ (if x ≥ 0 then x else -x)"

text {* Ejemplo, el valor absoluto de -3 es 3. *}

value "absoluto(-3)" -- "= 3"

text {* Def.: Un número natural n es un sucesor si es de la forma
(Suc m). *}

definition es_sucesor :: "nat ⇒ bool" where
"es_sucesor n ≡ (case n of
0 ⇒ False
| Suc m ⇒ True)"

text {* Ejemplo, el número 3 es sucesor. *}

value "es_sucesor 3" -- "= True"

section {* Tipos de datos y definiciones recursivas *}

text {* Una lista de elementos de tipo a es la lista Vacia o se obtiene
añadiendo, con Cons, un elemento de tipo a a una lista de elementos de
tipo a. *}

datatype 'a Lista = Vacia | Cons 'a "'a Lista"

text {* (conc xs ys) es la concatenación de las lista xs e ys. Por
ejemplo,
conc (Cons a (Cons b Vacia)) (Cons c Vacia)
= Cons a (Cons b (Cons c Vacia))
*}

fun conc :: "'a Lista ⇒ 'a Lista ⇒ 'a Lista" where
"conc Vacia ys = ys"
| "conc (Cons x xs) ys = Cons x (conc xs ys)"

value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
-- "= Cons a (Cons b (Cons c Vacia))"

text {* (suma n) es la suma de los primeros n números naturales. Por
ejemplo,
suma 3 = 6
*}

fun suma :: "nat ⇒ nat" where
"suma 0 = 0"
| "suma (Suc m) = (Suc m) + suma m"

value "suma 3" -- "= 6"

text {* (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 3 = 9
*}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n"

value "sumaImpares 3" -- "= 9"

end

</source>

Tema 14

2013-05-22T08:09:13Z

Mjoseh: Página creada con '<source lang = "isar"> header {* Tema 14: Programación funcional en Isabelle *} theory T14 imports Main begin section {* Introducción *} text {* En este tema se pres...'

<source lang = "isar">
header {* Tema 14: Programación funcional en Isabelle *}

theory T14
imports Main
begin

section {* Introducción *}

text {*
En este tema se presenta el lenguaje funcional que está
incluido en Isabelle. El lenguaje funcional es muy parecido a
Haskell. *}

section {* Números naturales, enteros y booleanos *}

text {* En Isabelle están definidos los número naturales con la sintaxis
de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).

Los números como el 1 son abreviaturas de los correspondientes en la
notación de Peano, en este caso "Suc 0".

El tipo de los números naturales es nat.

Por ejemplo, el siguiente del 0 es el 1. *}

value "Suc 0" -- "= 1"

text {* En Isabelle está definida la suma de los números naturales:
(x + y) es la suma de x e y.

Por ejemplo, la suma de los números naturales 1 y 2 es el número
natural 3. *}

value "(1::nat) + 2" -- "= 3"

text {* La notación del par de dos puntos se usa para asignar un tipo a
un término (por ejemplo, (1::nat) significa que se considera que 1 es
un número natural).

En Isabelle está definida el producto de los números naturales:
(x * y) es el producto de x e y.

Por ejemplo, el producto de los números naturales 2 y 3 es el número
natural 6. *}

value "(2::nat) * 3" -- "= 6"

text {* En Isabelle está definida la división de números naturales:
(n div m) es el cociente entero de x entre y.

Por ejemplo, la división natural de 7 entre 3 es 2. *}

value "(7::nat) div 3" -- "= 2"

text {* En Isabelle está definida el resto de división de números
naturales: (n mod m) es el resto de dividir n entre m.

Por ejemplo, el resto de dividir 7 entre 3 es 1. *}

value "(7::nat) mod 3" -- "= 1"

text {* En Isabelle también están definidos los números enteros. El tipo
de los enteros se representa por int.

Por ejemplo, la suma de 1 y -2 es el número entero -1. *}

value "(1::int) + -2" -- "= -1"

text {* Los numerales están sobrecargados. Por ejemplo, el 1 puede ser
un natural o un entero, dependiendo del contexto.

Isabelle resuelve ambigüedades mediante inferencia de tipos.

A veces, es necesario usar declaraciones de tipo para resolver la
ambigüedad.

En Isabelle están definidos los valores booleanos (True y False), las
conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃).

El tipo de los booleanos es bool. *}

text {* La conjunción de dos fórmulas verdaderas es verdadera. *}
value "True \<and> True" -- "= True"

text {* La conjunción de un fórmula verdadera y una falsa es falsa. *}
value "True \<and> False" -- "= False"

text {* La disyunción de una fórmula verdadera y una falsa es
verdadera. *}
value "True \<or> False" -- "= True"

text {* La disyunción de dos fórmulas falsas es falsa. *}
value "False \<or> False" -- "= False"

text {* La negación de una fórmula verdadera es falsa. *}
value "\<not>True" -- "= False"

text {* Una fórmula falsa implica una fórmula verdadera. *}
value "False \<longrightarrow> True" -- "= True"

text {* Un lema introduce una proposición seguida de una demostración.

Isabelle dispone de varios procedimientos automáticos para generar
demostraciones, uno de los cuales es el de simplificación (llamado
simp).

El procedimiento simp aplica un conjunto de reglas de reescritura, que
inicialmente contiene un gran número de reglas relativas a los objetos
definidos. *}

text {* Ej. de simp: Todo elemento es igual a sí mismo. *}
lemma "\<forall>x. x = x"
by simp

text {* Ej. de simp: Existe un elemento igual a 1. *}
lemma "\<exists>x. x = 1"
by simp

section {* Definiciones no recursivas *}

text {* La disyunción exclusiva de A y B se verifica si una es verdadera
y la otra no lo es. *}

definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"

text {* Prop.: La disyunción exclusiva de dos fórmulas verdaderas es
falsa.

Dem.: Por simplificación, usando la definición de la disyunción
exclusiva.
*}

lemma "xor True True = False"
by (simp add: xor_def)

text {* Se añade la definición de la disyunción exclusiva al conjunto de
reglas de simplificación automáticas. *}

declare xor_def[simp]

lemma "xor True False = True"
by simp

section {* Definiciones locales *}

text {* Se puede asignar valores a variables locales mediante 'let' y
usarlo en las expresiones dentro de 'in'.

Por ejemplo, si x es el número natural 3, entonces "x*x=9". *}

value "let x = 3::nat in x * x" -- "= 9"

section {* Pares *}

text {* Un par se representa escribiendo los elementos entre paréntesis
y separados por coma.

El tipo de los pares es el producto de los tipos.

La función fst devuelve el primer elemento de un par y la snd el
segundo.

Por ejemplo, si p es el par de números naturales (2,3), entonces la
suma del primer elemento de p y 1 es igual al segundo elemento de
p. *}

value "let p = (2,3)::nat \<times> nat in fst p + 1 = snd p"

section {* Listas *}

text {* Una lista se representa escribiendo los elementos entre
corchetes y separados por comas.

La lista vacía se representa por [].

Todos los elementos de una lista tienen que ser del mismo tipo.

El tipo de las listas de elementos del tipo a es (a list).

El término (x#xs) representa la lista obtenida añadiendo el elemento x
al principio de la lista xs.

Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista
vacía los elementos c, b y a es [a,b,c]. *}

value "a#(b#(c#[]))" -- "= [a,b,c]"

text {* Funciones de descomposión de listas:
· (hd xs) es el primer elemento de la lista xs.
· (tl xs) es el resto de la lista xs.

Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a
y el resto de xs es [b,c]. *}

value "let xs = [a,b,c] in hd xs = a \<and> tl xs = [b,c]" -- "= True"

text {* (length xs) es la longitud de la lista xs. Por ejemplo, la
longitud de la lista [1,2,3] es 3. *}

value "length [1,2,3]" -- "= 3"

text {* En la sesión 47 de "Isabelle/HOL — Higher-Order Logic"
http://goo.gl/sFsFF se encuentran más definiciones y propiedades de
las listas. *}

section {* Registros *}

text {* Un registro es una colección de campos y valores.

Por ejemplo, los puntos del plano se pueden representar mediante
registros con dos campos, las coordenadas, con valores enteros. *}

record punto =
coordenada_x :: int
coordenada_y :: int

text {* Ejemplo, el punto pt tiene de coordenadas 3 y 7. *}

definition pt :: punto where
"pt \<equiv> \<lparr>coordenada_x = 3, coordenada_y = 7\<rparr>"

text {* Ejemplo, la coordenada x del punto pt es 3. *}

value "coordenada_x pt" -- "= 3"

text {* Ejemplo, sea pt2 el punto obtenido a partir del punto pt
cambiando el valor de su coordenada x por 4. Entonces la coordenada x
del punto pt2 es 4. *}

value "let pt2 = pt\<lparr>coordenada_x:=4\<rparr> in coordenada_x (pt2)" -- "= 4"

section {* Funciones anónimas *}

text {* En Isabelle pueden definirse funciones anónimas.

Por ejemplo, el valor de la función que a un número le asigna su doble
aplicada a 1 es 2. *}

value "(\<lambda>x. x + x) 1::nat" -- "= 2"

section {* Condicionales *}

text {* El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso
contrario. *}

definition absoluto :: "int \<Rightarrow> int" where
"absoluto x \<equiv> (if x \<ge> 0 then x else -x)"

text {* Ejemplo, el valor absoluto de -3 es 3. *}

value "absoluto(-3)" -- "= 3"

text {* Def.: Un número natural n es un sucesor si es de la forma
(Suc m). *}

definition es_sucesor :: "nat \<Rightarrow> bool" where
"es_sucesor n \<equiv> (case n of
0 \<Rightarrow> False
| Suc m \<Rightarrow> True)"

text {* Ejemplo, el número 3 es sucesor. *}

value "es_sucesor 3" -- "= True"

section {* Tipos de datos y definiciones recursivas *}

text {* Una lista de elementos de tipo a es la lista Vacia o se obtiene
añadiendo, con Cons, un elemento de tipo a a una lista de elementos de
tipo a. *}

datatype 'a Lista = Vacia | Cons 'a "'a Lista"

text {* (conc xs ys) es la concatenación de las lista xs e ys. Por
ejemplo,
conc (Cons a (Cons b Vacia)) (Cons c Vacia)
= Cons a (Cons b (Cons c Vacia))
*}

fun conc :: "'a Lista \<Rightarrow> 'a Lista \<Rightarrow> 'a Lista" where
"conc Vacia ys = ys"
| "conc (Cons x xs) ys = Cons x (conc xs ys)"

value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
-- "= Cons a (Cons b (Cons c Vacia))"

text {* (suma n) es la suma de los primeros n números naturales. Por
ejemplo,
suma 3 = 6
*}

fun suma :: "nat \<Rightarrow> nat" where
"suma 0 = 0"
| "suma (Suc m) = (Suc m) + suma m"

value "suma 3" -- "= 6"

text {* (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 3 = 9
*}

fun sumaImpares :: "nat \<Rightarrow> nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n"

value "sumaImpares 3" -- "= 9"

end

</source>

Lógica matemática y fundamentos

2013-05-22T08:06:24Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).

=== Teorías Isabelle/HOL de los temas de deducción natural ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]] ([[Media:T14.thy |Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]].

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Lógica matemática y fundamentos

2013-05-22T08:06:00Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).

=== Teorías Isabelle/HOL de los temas de deducción natural ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]] ([[Media: T14.thy | Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]].

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Lógica matemática y fundamentos

2013-05-22T08:05:25Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).

=== Teorías Isabelle/HOL de los temas de deducción natural ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]], [[Media: T14.thy | Teoría]].
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]].

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Lógica matemática y fundamentos

2013-05-22T08:04:19Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).

=== Teorías Isabelle/HOL de los temas de deducción natural ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Tema 14''': ([[Tema 14 | Programación funcional en Isabelle/HOL]], [[Media: T14.thy | Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]].

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

AplicacionesLP

2013-05-21T07:06:58Z

Mjoseh: Página creada con '<source lang = "haskell"> -- AplicacionesLP.hs -- Aplicaciones de la Lógica proposicional. -- --------------------------------------------------------------------- -- --------...'

<source lang = "haskell">
-- AplicacionesLP.hs
-- Aplicaciones de la Lógica proposicional.
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Librerías auxiliares --
-- ---------------------------------------------------------------------

import SintaxisSemantica
-- import TablerosSemanticos
-- import ResolucionProposicional

-- ---------------------------------------------------------------------
-- Ejercicio 1: En una isla hay dos tribus, la de los veraces (que
-- siempre dicen la verdad) y la de los mentirosos (que siempre
-- mienten). Un viajero se encuentra con tres isleños A, B y C y cada
-- uno le dice una frase A dice “B y C son veraces syss C es veraz” B
-- dice “Si A y B son veraces, entonces B y C son veraces y A es
-- mentiroso” C dice “B es mentiroso syss A o B es veraz”
--
-- Determinar a qué tribu pertenecen A, B y C.

-- Simbolización:
-- a, b y c representan que A, B y C son veraces
-- -a, -b y -c representan que A, B y C son mentirosos
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 2: Decidir si es posible colorear los vértices de un
-- pentágono de rojo o azul de forma que los vértices adyacentes
-- tengan colores distintos.

-- Simbolización:
-- 1, 2, 3, 4, 5 representan los vértices consecutivos del pentágono
-- ri (1 ≤ i ≤ 5) representa que el vértice i es rojo
-- ai (1 ≤ i ≤ 5) representa que el vértice i es azul
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 3: Cuatro palomas comparten tres huecos. Decidir si es
-- posible que no haya dos palomas en el mismo hueco.

-- Simbolización:
-- pihj (i ∈ {1, 2, 3, 4} y j ∈ {1, 2, 3}) representa
-- que la paloma i está en el hueco j.
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Un rectángulo se divide en seis rectángulos menores como
-- se indica en la figura.

-- ------------------
-- | | B |
-- | A |----------
-- | | | |
-- |------| D | |
-- | C | | E |
-- |------|---| |
-- | F | |
-- ------------------

-- Demostrar que si cada una de los rectángulos menores tiene un lado
-- cuya medida es un número entero, entonces la medida de alguno de los
-- lados del rectángulo mayor es un número entero.

-- Simbolización:
-- base: la base del rectángulo mayor es un número entero
-- altura: la altura del rectángulo mayor es un número entero
-- base_x: la base del rectángulo X es un número entero
-- altura_x: la altura del rectángulo X es un número entero
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Calcular las formas de colocar 4 reinas en un tablero
-- de 4x4 de forma que no haya más de una reina en cada fila,
-- columna o diagonal.

-- Simbolización:
-- cij (1 ≤ i, j ≤ 4) indica que hay una reina en la fila i columna j.
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Probar el caso más simple del teorema de Ramsey: entre
-- seis personas siempre hay (al menos) tres tales que cada una conoce
-- a las otras dos o cada una no conoce a ninguna de las otras dos.

-- Simbolización:
-- 1,2,3,4,5,6 representan a las personas
-- pij (1 ≤ i < j ≤ 6) indica que las personas i y j se conocen.
-- ---------------------------------------------------------------------
</source>

Archivo:AplicacionesLP.hs

2013-05-21T07:06:17Z

Mjoseh:

Lógica matemática y fundamentos

2013-05-21T07:05:51Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).
* '''Relación 12''': Aplicaciones de la Lógica Proposicional en Haskell. ([[Media:AplicacionesLP.hs |Enunciado]] y [[AplicacionesLP |Solución colaborativa]]).

=== Teorías Isabelle/HOL de los temas de deducción natural ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Relación 11

2013-05-15T11:02:13Z

Mjoseh:

<source lang = "haskell">

-- ResolucionProposicional.hs
-- Resolución proposicional.
-- ---------------------------------------------------------------------

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

-- ---------------------------------------------------------------------
-- Resolventes --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
-- tal que (resolvente c1 c2 l) es la resolvente de c1 y c2 respecto del
-- literal l. Por ejemplo,
-- resolvente [no p,q] [no q,r] q ==> [no p,r]
-- resolvente [no p,no q] [q,r] (no q) ==> [no p,r]
-- resolvente [no p,q] [no p,no q] q ==> [no p]
-- ---------------------------------------------------------------------

--Jose M Contreras

resolvente :: Clausula -> Clausula -> Literal -> Clausula
resolvente c1 c2 x = union (delete x c1) (delete (complementario x) c2)
--La función complementario se define en el fichero importado FormasNormales

--Miriam Núñez-Romero

resolvente2 :: Clausula -> Clausula -> Literal -> Clausula
resolvente2 c1 c2 l = delete l (delete (complementario l) (c1`union`c2))
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Cláusula -> Cláusula -> [Cláusula]
-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y
-- c2. Por ejemplo,
-- resolventes [no p,q] [p,no q] ==> [[q,no q],[no p,p]]
-- resolventes [no p,q] [p,q] ==> [[q]]
-- ---------------------------------------------------------------------

--Jose M Contreras

resolventes :: Clausula -> Clausula -> [Clausula]
resolventes c1 c2 = [resolvente c1 c2 x| x<-c1, elem (complementario x) c2]

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo,
-- resolventesCláusulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
-- ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------

--Jose M Contreras

resolventesClausulaConjunto :: Clausula -> [Clausula] -> [Clausula]
resolventesClausulaConjunto c s = unionGeneral [resolventes c x|x<-s]

-- ---------------------------------------------------------------------
-- Eliminación de tautologías --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esTautología :: Cláusula -> Bool
-- tal que (esTautología c) se verifica si c es una tautología. Por
-- ejemplo,
-- esTautología [p, q, no p] ==> True
-- esTautología [p, q, no r] ==> False
-- esTautología [] ==> False
-- ---------------------------------------------------------------------

--Jose M Contreras

esTautologia :: Clausula -> Bool
esTautologia c = or[elem (complementario x) (delete x c)|x<-c]

--Miriam Núñez-Romero
esTautologia2 :: Clausula -> Bool
esTautologia2 c = or [elem (complementario x) c |x<-c]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaTautologías :: [Cláusula] -> [Cláusula]
-- tal que (eliminaTautologías s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
-- eliminaTautologías [[p, q], [p, q, no p]] ==> [[p,q]]
-- ---------------------------------------------------------------------

--Jose M Contreras

eliminaTautologias :: [Clausula] -> [Clausula]
eliminaTautologias s = [x|x<-s, not(esTautologia x)]

-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- esInconsistentePorResolución :: [Cláusula] -> Bool
-- tal que (esInconsistentePorResolución s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
-- esInconsistentePorResolución [[p],[no p,q],[no q]]
-- ==> True
-- esInconsistentePorResolución [[p],[no p,q]]
-- ==> False
-- esInconsistentePorResolución [[p,q],[no p,q],[p,no q],[no p,no q]]
-- ==> True
-- esInconsistentePorResolución [[p,q],[p,r],[no q,no r],[no p]]
-- ==> True
-- ---------------------------------------------------------------------

esInconsistentePorResolución :: [Cláusula] -> Bool
esInconsistentePorResolución s =
esInconsistentePorResolución' s []

esInconsistentePorResolución' :: [Cláusula] -> [Cláusula] -> Bool
esInconsistentePorResolución' soporte usables
| null soporte = False
| elem [] soporte = True
| otherwise =
esInconsistentePorResolución' soporte' usables'
where actual = head soporte
usables' = union [actual] usables
soporte' = union (tail soporte)
[c
| c <- resolventesCláusulaConjunto
actual
usables'
, not (esTautología c)
, notElem c soporte
, notElem c usables']

-- ---------------------------------------------------------------------
-- Validez mediante resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- esVálidaPorResolución :: Prop -> Bool
-- tal que (esVálidaPorResolución f) se verifica si f es válida por
-- resolución. Por ejemplo,
-- esVálidaPorResolución (p --> p) ==> True
-- esVálidaPorResolución ((p --> q) \/ (q --> p)) ==> True
-- esVálidaPorResolución (p --> q) ==> False
-- ---------------------------------------------------------------------

esVálidaPorResolución :: Prop -> Bool
esVálidaPorResolución f = undefined

-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolución s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
-- esConsecuenciaPorResolución [p --> q, q --> r] (p --> r)
-- ==> True
-- esConsecuenciaPorResolución [p --> q, q --> r] (p <--> r)
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolución s f = undefined

</source>

Ejercicio 4

2013-05-15T10:30:34Z

Mjoseh:

== Enunciado ==
El cuarto ejercicio evaluable consiste una de las dos opciones que se ofrecen a
continuación:

* Programación en Haskell de algunos de los refinamientos de resolución en lógica proposicional. Las funciones finales han de ser (esValidaPorResolucion* f) para determinar la validez de la fórmula f; y (esConsecuenciaPoResolucion* s f) que determine si la fórmula f es consecuencia lógica del conjunto s, siendo * el refinamiento correspondiente. Esta opción tendrá peso 4 en el cálculo de la calificación por curso.

* Programación en Haskell del algoritmo de Davis-Putnam. Las funciones finales han de ser (esValidaPorDP f) para determinar la validez de la fórmula f; y (esConsecuenciaPorDP s f) que determine si la fórmula f es consecuencia lógica del conjunto s. Esta opción tendrá peso 5 en el cálculo de la calificación por curso.

En ambos casos hay que usar la representación de la lógica proposicional en
Haskell, realizada en las relaciones de ejercicios 2, 9 y 10. Se valorará la
estructura y la eficiencia de las funciones, así como la claridad de los
comentarios.

Se enviará a mjoseh@us.es antes del viernes 31 de mayo de 2013 un fichero
usuario_4a.hs o usuario_4b.hs, según la opción elegida.

Ejercicio 4

2013-05-15T10:30:23Z

Mjoseh:

Ejercicio 4

2013-05-15T10:29:49Z

Mjoseh:

== Enunciado ==
El cuarto ejercicio evaluable consiste una de las dos opciones que se ofrecen a
continuación:

* Programación en Haskell de algunos de los refinamientos de resolución en lógica proposicional. Las funciones finales han de ser (esValidaPorResolucion* f) para determinar la validez de la fórmula f; y (esConsecuenciaPoResolucion* s f) que determine si la fórmula f es consecuencia lógica del conjunto s, siendo * el refinamiento correspondiente. Esta opción tendrá peso 4 en el cálculo de la calificación por curso.

* Programación en Haskell del algoritmo de Davis-Putnam. Las funciones
finales han de ser (esValidaPorDP f) para determinar la validez de la fórmula
f; y (esConsecuenciaPorDP s f) que determine si la fórmula f es consecuencia
lógica del conjunto s. Esta opción tendrá peso 5 en el cálculo de la
calificación por curso.

En ambos casos hay que usar la representación de la lógica proposicional en
Haskell, realizada en las relaciones de ejercicios 2, 9 y 10. Se valorará la
estructura y la eficiencia de las funciones, así como la claridad de los
comentarios.

Se enviará a mjoseh@us.es antes del viernes 31 de mayo de 2013 un fichero
usuario_4a.hs o usuario_4b.hs, según la opción elegida.

Ejercicio 4

2013-05-15T10:28:31Z

Mjoseh:

== Enunciado ==
El cuarto ejercicio evaluable consiste una de las dos opciones que se ofrecen a
continuación:

* Programación en Haskell de algunos de los refinamientos de resolución en
lógica proposicional. Las funciones finales han de ser (esValidaPorResolucion*
f) para determinar la validez de la fórmula f; y (esConsecuenciaPoResolucion*
s f) que determine si la fórmula f es consecuencia lógica del conjunto s,
siendo * el refinamiento correspondiente. Esta opción tendrá peso 4 en el
cálculo de la calificación por curso.

* Programación en Haskell del algoritmo de Davis-Putnam. Las funciones
finales han de ser (esValidaPorDP f) para determinar la validez de la fórmula
f; y (esConsecuenciaPorDP s f) que determine si la fórmula f es consecuencia
lógica del conjunto s. Esta opción tendrá peso 5 en el cálculo de la
calificación por curso.

En ambos casos hay que usar la representación de la lógica proposicional en
Haskell, realizada en las relaciones de ejercicios 2, 9 y 10. Se valorará la
estructura y la eficiencia de las funciones, así como la claridad de los
comentarios.

Se enviará a mjoseh@us.es antes del viernes 31 de mayo de 2013 un fichero
usuario_4a.hs o usuario_4b.hs, según la opción elegida.

Ejercicio 4

2013-05-15T10:27:26Z

Mjoseh: Página creada con 'El cuarto ejercicio evaluable consiste una de las dos opciones que se ofrecen a continuación: 1.- Programación en Haskell de algunos de los refinamientos de resolución en l...'

El cuarto ejercicio evaluable consiste una de las dos opciones que se ofrecen a
continuación:

1.- Programación en Haskell de algunos de los refinamientos de resolución en
lógica proposicional. Las funciones finales han de ser (esValidaPorResolucion*
f) para determinar la validez de la fórmula f; y (esConsecuenciaPoResolucion*
s f) que determine si la fórmula f es consecuencia lógica del conjunto s,
siendo * el refinamiento correspondiente. Esta opción tendrá peso 4 en el
cálculo de la calificación por curso.

2.- Programación en Haskell del algoritmo de Davis-Putnam. Las funciones
finales han de ser (esValidaPorDP f) para determinar la validez de la fórmula
f; y (esConsecuenciaPorDP s f) que determine si la fórmula f es consecuencia
lógica del conjunto s. Esta opción tendrá peso 5 en el cálculo de la
calificación por curso.

En ambos casos hay que usar la representación de la lógica proposicional en
Haskell, realizada en las relaciones de ejercicios 2, 9 y 10. Se valorará la
estructura y la eficiencia de las funciones, así como la claridad de los
comentarios.

Se enviará a mjoseh@us.es antes del viernes 31 de mayo de 2013 un fichero
usuario_4a.hs o usuario_4b.hs, según la opción elegida.

Lógica matemática y fundamentos

2013-05-15T10:26:54Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).

=== Teorías Isabelle/HOL de los temas de deducción natural ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].
* '''Ejercicio 4''': [[Ejercicio 4 | Algoritmos de lógica proposicional en Haskell]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

Relación 11

2013-05-02T09:05:43Z

Mjoseh: Página creada con '<source lang = "haskell"> -- ResolucionProposicional.hs -- Resolución proposicional. -- --------------------------------------------------------------------- module Resolucio...'

<source lang = "haskell">

-- ResolucionProposicional.hs
-- Resolución proposicional.
-- ---------------------------------------------------------------------

module ResolucionProposicional where

import SintaxisSemantica
import FormasNormales
import Clausulas
import Data.List

-- ---------------------------------------------------------------------
-- Resolventes --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
-- tal que (resolvente c1 c2 l) es la resolvente de c1 y c2 respecto del
-- literal l. Por ejemplo,
-- resolvente [no p,q] [no q,r] q ==> [no p,r]
-- resolvente [no p,no q] [q,r] (no q) ==> [no p,r]
-- resolvente [no p,q] [no p,no q] q ==> [no p]
-- ---------------------------------------------------------------------

resolvente :: Cláusula -> Cláusula -> Literal -> Cláusula
resolvente c1 c2 l = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- resolventes :: Cláusula -> Cláusula -> [Cláusula]
-- tal que (resolventes c1 c2) es el conjunto de las resolventes de c1 y
-- c2. Por ejemplo,
-- resolventes [no p,q] [p,no q] ==> [[q,no q],[no p,p]]
-- resolventes [no p,q] [p,q] ==> [[q]]
-- ---------------------------------------------------------------------

resolventes :: Cláusula -> Cláusula -> [Cláusula]
resolventes c1 c2 = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
-- tal que (resolventes c s) es el conjunto de las resolventes de c y
-- s. Por ejemplo,
-- resolventesCláusulaConjunto [no p,q] [[p,q],[p,r],[no q,s]]
-- ==> [[q],[q,r],[no p,s]]
-- ---------------------------------------------------------------------

resolventesCláusulaConjunto :: Cláusula -> [Cláusula] -> [Cláusula]
resolventesCláusulaConjunto c s = undefined

-- ---------------------------------------------------------------------
-- Eliminación de tautologías --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esTautología :: Cláusula -> Bool
-- tal que (esTautología c) se verifica si c es una tautología. Por
-- ejemplo,
-- esTautología [p, q, no p] ==> True
-- esTautología [p, q, no r] ==> False
-- esTautología [] ==> False
-- ---------------------------------------------------------------------

esTautología :: Cláusula -> Bool
esTautología c = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaTautologías :: [Cláusula] -> [Cláusula]
-- tal que (eliminaTautologías s) es el conjunto obtenido eliminando las
-- tautologías de s. Por ejemplo,
-- eliminaTautologías [[p, q], [p, q, no p]] ==> [[p,q]]
-- ---------------------------------------------------------------------

eliminaTautologías :: [Cláusula] -> [Cláusula]
eliminaTautologías s = undefined

-- ---------------------------------------------------------------------
-- Decisión de inconsistencia por resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- esInconsistentePorResolución :: [Cláusula] -> Bool
-- tal que (esInconsistentePorResolución s) se verifica si s es
-- inconsistente mediante resolución. Por ejemplo,
-- esInconsistentePorResolución [[p],[no p,q],[no q]]
-- ==> True
-- esInconsistentePorResolución [[p],[no p,q]]
-- ==> False
-- esInconsistentePorResolución [[p,q],[no p,q],[p,no q],[no p,no q]]
-- ==> True
-- esInconsistentePorResolución [[p,q],[p,r],[no q,no r],[no p]]
-- ==> True
-- ---------------------------------------------------------------------

esInconsistentePorResolución :: [Cláusula] -> Bool
esInconsistentePorResolución s = undefined

-- ---------------------------------------------------------------------
-- Validez mediante resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- esVálidaPorResolución :: Prop -> Bool
-- tal que (esVálidaPorResolución f) se verifica si f es válida por
-- resolución. Por ejemplo,
-- esVálidaPorResolución (p --> p) ==> True
-- esVálidaPorResolución ((p --> q) \/ (q --> p)) ==> True
-- esVálidaPorResolución (p --> q) ==> False
-- ---------------------------------------------------------------------

esVálidaPorResolución :: Prop -> Bool
esVálidaPorResolución f = undefined

-- ---------------------------------------------------------------------
-- Consecuencia mediante resolución --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorResolución s f) se verifica si f es
-- consecuencia de s mediante el método de resolución. Por ejemplo,
-- esConsecuenciaPorResolución [p --> q, q --> r] (p --> r)
-- ==> True
-- esConsecuenciaPorResolución [p --> q, q --> r] (p <--> r)
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaPorResolución :: [Prop] -> Prop -> Bool
esConsecuenciaPorResolución s f = undefined

</source>

Relación 10

2013-05-02T09:05:02Z

Mjoseh: Página creada con '<source lang = "haskell"> -- Clausulas.hs -- Cláusulas. -- --------------------------------------------------------------------- module Clausulas where -- -------------------...'

<source lang = "haskell">
-- Clausulas.hs
-- Cláusulas.
-- ---------------------------------------------------------------------

module Clausulas where

-- ---------------------------------------------------------------------
-- Librería suxiliares --
-- ---------------------------------------------------------------------

import SintaxisSemantica
import FormasNormales
import Data.List

-- ---------------------------------------------------------------------
-- Cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir el tipo de datos Cláusula como una lista de
-- literales.
-- ---------------------------------------------------------------------

type Cláusula = [Literal]

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- cláusula :: Prop -> Cláusula
-- tal que (cláusula f) es la cláusula de la fórmula-clausal f. Por
-- ejemplo,
-- cláusula p ==> [p]
-- cláusula (no p) ==> [no p]
-- cláusula (((no p) \/ r) \/ ((no p) \/ q)) ==> [q,r,no p]
-- ---------------------------------------------------------------------

cláusula :: Prop -> Cláusula
cláusula f = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- cláusulasFNC :: Prop -> [Cláusula]
-- tal que (cláusulasFNC f) es el conjunto de cláusulas de la fórmula en
-- forma normal conjuntiva f. Por ejmplo,
-- cláusulasFNC (p /\ ((no q) \/ r))
-- ==> [[p],[r, no q]]
-- cláusulasFNC (((no p) \/ q) /\ ((no p) \/ (no r)))
-- ==> [[q, no p],[no p,no r]]
-- ---------------------------------------------------------------------

cláusulasFNC :: Prop -> [Cláusula]
cláusulasFNC = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- cláusulas :: Prop -> [Cláusula]
-- tal que (cláusulas f) es un conjunto de cláusulas equivalente a
-- f. Por ejemplo,
-- cláusulas (p /\ (q --> r))
-- ==> [[p],[r,no q]]
-- cláusulas (no (p /\ (q --> r)))
-- ==> [[q,no p],[no p,no r]]
-- cláusulas (no(p <--> r))
-- ==> [[p,r],[p,no p],[r,no r],[no p,no r]]
-- ---------------------------------------------------------------------

cláusulas :: Prop -> [Cláusula]
cláusulas f = undefined

-- ---------------------------------------------------------------------
-- Cláusulas de un conjunto de fórmulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- cláusulasConjunto :: [Prop] -> [Cláusula]
-- tal que (cláusulasConjunto s) es un conjunto de cláusulas equivalente
-- a s. Por ejemplo,
-- cláusulasConjunto [p --> q, q --> r] ==> [[q,no p],[r,no q]]
-- cláusulasConjunto [p --> q, q <--> p] ==> [[q,no p],[p,no q]]
-- ---------------------------------------------------------------------

cláusulasConjunto :: [Prop] -> [Cláusula]
cláusulasConjunto s = undefined

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de una cláusula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- símbolosProposicionalesCláusula :: Cláusula -> [Prop]
-- tal que (símbolosProposicionalesCláusula c) es el conjunto de los
-- símbolos proposicionales de c. Por ejemplo,
-- símbolosProposicionalesCláusula [p, q, no p] ==> [p,q]
-- ---------------------------------------------------------------------

símbolosProposicionalesCláusula :: Cláusula -> [Prop]
símbolosProposicionalesCláusula = undefined

-- ---------------------------------------------------------------------
-- Símbolos proposicionales de un conjunto de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir la función
-- símbolosProposicionalesConjuntoCláusula :: [Cláusula] -> [Prop]
-- tal que (símbolosProposicionalesConjuntoCláusula s) es el conjunto de los
-- símbolos proposicionales de s. Por ejemplo,
-- símbolosProposicionalesConjuntoCláusula [[p, q],[no q, r]]
-- ==> [p,q,r]
-- ---------------------------------------------------------------------

símbolosProposicionalesConjuntoCláusula :: [Cláusula] -> [Prop]
símbolosProposicionalesConjuntoCláusula s = undefined

-- ---------------------------------------------------------------------
-- Interpretaciones de una cláusula --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- interpretacionesCláusula :: Cláusula -> [Interpretación]
-- tal que (interpretacionesCláusula c) es el conjunto de
-- interpretaciones de c. Por ejemplo,
-- interpretacionesCláusula [p, q, no p] ==> [[p,q],[p],[q],[]]
-- interpretacionesCláusula [] ==> [[]]
-- ---------------------------------------------------------------------

interpretacionesCláusula :: Cláusula -> [Interpretación]
interpretacionesCláusula c = undefined

-- ---------------------------------------------------------------------
-- Interpretaciones de un conjunto de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- interpretacionesConjuntoCláusula :: [Cláusula] -> [Interpretación]
-- tal que (interpretacionesConjuntoCláusula s) es el conjunto de
-- interpretaciones de s. Por ejemplo,
-- interpretacionesConjuntoCláusula [[p, no q],[no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- interpretacionesConjuntoCláusula []
-- ==> [[]]
-- ---------------------------------------------------------------------

interpretacionesConjuntoCláusula :: [Cláusula] -> [Interpretación]
interpretacionesConjuntoCláusula c = undefined

-- ---------------------------------------------------------------------
-- Modelos de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- esModeloLiteral :: Interpretación -> Literal -> Bool
-- tal que (esModeloLiteral i l) se verifica si i es modelo de l. Por
-- ejemplo,
-- esModeloLiteral [p,r] p ==> True
-- esModeloLiteral [p,r] q ==> False
-- esModeloLiteral [p,r] (no p) ==> False
-- esModeloLiteral [p,r] (no q) ==> True
-- ---------------------------------------------------------------------

esModeloLiteral :: Interpretación -> Literal -> Bool
esModeloLiteral = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- esModeloCláusula :: Interpretación -> Cláusula -> Bool
-- tal que (esModeloCláusula i c) se verifica si i es modelo de c . Por
-- ejemplo,
-- esModeloCláusula [p,r] [p, q] ==> True
-- esModeloCláusula [r] [p, no q] ==> True
-- esModeloCláusula [q,r] [p, no q] ==> False
-- esModeloCláusula [q,r] [] ==> False
-- ---------------------------------------------------------------------

esModeloCláusula :: Interpretación -> Cláusula -> Bool
esModeloCláusula i c = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- modelosCláusula :: Cláusula -> [Interpretación]
-- tal que (modelosCláusula c) es la lista de los modelos de c. Por
-- ejemplo,
-- modelosCláusula [no p, q] ==> [[p,q],[q],[]]
-- modelosCláusula [no p, p] ==> [[p],[]]
-- modelosCláusula [] ==> []
-- ---------------------------------------------------------------------

modelosCláusula :: Cláusula -> [Interpretación]
modelosCláusula c = undefined

-- ---------------------------------------------------------------------
-- Modelos de conjuntos de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- esModeloConjuntoCláusulas :: Interpretación -> [Cláusula] -> Bool
-- tal que (esModeloConjuntoCláusulas i c) se verifica si i es modelo de
-- c. Por ejemplo,
-- esModeloConjuntoCláusulas [p,r] [[p, no q], [r]] ==> True
-- esModeloConjuntoCláusulas [p] [[p, no q], [r]] ==> False
-- esModeloConjuntoCláusulas [p] [] ==> True
-- ---------------------------------------------------------------------

esModeloConjuntoCláusulas :: Interpretación -> [Cláusula] -> Bool
esModeloConjuntoCláusulas i s = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 14: Definir la función
-- modelosConjuntoCláusulas :: [Cláusula] -> [Interpretación]
-- tal que (modelosConjuntoCláusulas s) es la lista de los modelos de
-- s. Por ejemplo,
-- modelosConjuntoCláusulas [[no p, q], [no q, p]]
-- ==> [[p,q],[]]
-- modelosConjuntoCláusulas [[no p, q], [p], [no q]]
-- ==> []
-- modelosConjuntoCláusulas [[p, no p, q]]
-- ==> [[p,q],[p],[q],[]]
-- ---------------------------------------------------------------------

modelosConjuntoCláusulas :: [Cláusula] -> [Interpretación]
modelosConjuntoCláusulas s = undefined

-- ---------------------------------------------------------------------
-- Cláusulas válidas, satisfacibles e insatisfacibles --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 15: Definir la función
-- esCláusulaVálida :: Cláusula -> Bool
-- tal que (esCláusulaVálida c) se verifica si la cláusula c es
-- válida. Por ejemplo,
-- esCláusulaVálida [p, q, no p] ==> True
-- esCláusulaVálida [p, q, no r] ==> False
-- esCláusulaVálida [] ==> False
-- ---------------------------------------------------------------------

esCláusulaVálida :: Cláusula -> Bool
esCláusulaVálida c = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 16: Definir la función
-- esCláusulaInsatisfacible :: Cláusula -> Bool
-- tal que (esCláusulaInsatisfacible c) se verifica si la cláusula c es
-- insatisfacible. Por ejemplo,
-- esCláusulaInsatisfacible [p, q, no p] ==> False
-- esCláusulaInsatisfacible [p, q, no r] ==> False
-- esCláusulaInsatisfacible [] ==> True
-- ---------------------------------------------------------------------

esCláusulaInsatisfacible :: Cláusula -> Bool
esCláusulaInsatisfacible c = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 17: Definir la función
-- esCláusulaSatisfacible :: Cláusula -> Bool
-- tal que (esCláusulaSatisfacible c) se verifica si la cláusula c es
-- satisfacible. Por ejemplo,
-- esCláusulaSatisfacible [p, q, no p] ==> True
-- esCláusulaSatisfacible [p, q, no r] ==> True
-- esCláusulaSatisfacible [] ==> False
-- ---------------------------------------------------------------------

esCláusulaSatisfacible :: Cláusula -> Bool
esCláusulaSatisfacible c = undefined

-- ---------------------------------------------------------------------
-- Conjuntos válidos, consistentes e inconsistentes de cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 18: Definir la función
-- esConjuntoVálidoDeCláusulas :: [Cláusula] -> Bool
-- tal que (esConjuntoVálidoDeCláusulas s) se verifica si el conjunto de
-- cláusulas s es válido. Por ejemplo,
-- esConjuntoVálidoDeCláusulas [[no p, q], [no q, p]] ==> False
-- esConjuntoVálidoDeCláusulas [[no p, p], [no q, q]] ==> True
-- esConjuntoVálidoDeCláusulas [] ==> True
-- ---------------------------------------------------------------------

esConjuntoVálidoDeCláusulas :: [Cláusula] -> Bool
esConjuntoVálidoDeCláusulas s = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 19: Definir la función
-- esConjuntoConsistenteDeCláusulas :: [Cláusula] -> Bool
-- tal que (esConjuntoConsistenteDeCláusulas s) se verifica si el
-- conjunto de cláusulas s es consistente. Por ejemplo,
-- esConjuntoConsistenteDeCláusulas [[no p, q], [no q, p]] ==> True
-- esConjuntoConsistenteDeCláusulas [[no p, p], [no q, q]] ==> True
-- esConjuntoConsistenteDeCláusulas [] ==> True
-- ---------------------------------------------------------------------

esConjuntoConsistenteDeCláusulas :: [Cláusula] -> Bool
esConjuntoConsistenteDeCláusulas s = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 20: Definir la función
-- esConjuntoInconsistenteDeCláusulas :: [Cláusula] -> Bool
-- tal que (esConjuntoInconsistenteDeCláusulas s) se verifica si el
-- conjunto de cláusulas s es consistente. Por ejemplo,
-- esConjuntoInconsistenteDeCláusulas [[no p,q],[no q,p]] ==> False
-- esConjuntoInconsistenteDeCláusulas [[no p],[p]] ==> True
-- ---------------------------------------------------------------------

esConjuntoInconsistenteDeCláusulas :: [Cláusula] -> Bool
esConjuntoInconsistenteDeCláusulas s = undefined

-- ---------------------------------------------------------------------
-- Validez de fórmulas mediante cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 21: Definir la función
-- esVálidaPorCláusulas :: Prop -> Bool
-- tal que (esVálidaPorCláusulas f) se verifica si el conjunto de
-- cláusulas de f es válido. Por ejemplo,
-- esVálidaPorCláusulas (p --> q) ==> False
-- esVálidaPorCláusulas (p --> p) ==> True
-- esVálidaPorCláusulas ((p --> q) \/ (q --> p)) ==> True
-- ---------------------------------------------------------------------

esVálidaPorCláusulas :: Prop -> Bool
esVálidaPorCláusulas f = undefined

-- ---------------------------------------------------------------------
-- Consecuencia mediante cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 22: Definir la función
-- esConsecuenciaEntreCláusulas :: [Cláusula] -> [Cláusula] -> Bool
-- tal que (esConsecuenciaEntreCláusulas s1 s2) se verifica si todos los
-- modelos de s1 son modelos de s2. Por ejemplo,
-- esConsecuenciaEntreCláusulas [[no p,q],[no q,r]] [[no p,r]]
-- ==> True
-- esConsecuenciaEntreCláusulas [[p]] [[p],[q]]
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaEntreCláusulas :: [Cláusula] -> [Cláusula] -> Bool
esConsecuenciaEntreCláusulas s1 s2 = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 23: Definir la función
-- esConsecuenciaPorCláusulas1 :: [Prop] -> Prop -> Bool
-- tal que (esConsecuenciaPorCláusulas s f) se verifica si las cláusulas
-- de f son consecuencias de las de s. Por ejemplo,
-- esConsecuenciaPorCláusulas [(p --> q), (q --> r)] (p --> r)
-- ==> True
-- esConsecuenciaPorCláusulas [p] (p /\ q)
-- ==> False
-- ---------------------------------------------------------------------

esConsecuenciaPorCláusulas :: [Prop] -> Prop -> Bool
esConsecuenciaPorCláusulas s f = undefined

</source>

Archivo:FormasNormales.hs

2013-05-02T09:03:57Z

Mjoseh: subió una nueva versión de «Archivo:FormasNormales.hs»

Relación 9

2013-05-02T09:03:47Z

Mjoseh: Página creada con '<source lang = "haskell"> -- FormasNormales.hs -- Formas normales. -- --------------------------------------------------------------------- module FormasNormales where -- ----...'

<source lang = "haskell">
-- FormasNormales.hs
-- Formas normales.
-- ---------------------------------------------------------------------

module FormasNormales where

-- ---------------------------------------------------------------------
-- Librería suxiliares --
-- ---------------------------------------------------------------------

import SintaxisSemantica
import Data.List

-- ---------------------------------------------------------------------
-- Equivalencia lógica --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esEquivalente :: Prop -> Prop -> Bool
-- tal que (esEquivalente f g) se verifica si f y g son
-- equivalentes. Por ejemplo,
-- esEquivalente (p <--> q) ((p --> q) /\ (q --> p)) ==> True
-- esEquivalente (p --> q) ((no p) \/ q) ==> True
-- esEquivalente (p /\ q) (no ((no p) \/ (no q))) ==> True
-- esEquivalente (p \/ q) (no ((no p) /\ (no q))) ==> True
-- ---------------------------------------------------------------------

esEquivalente :: Prop -> Prop -> Bool
esEquivalente f g = undefined

-- ---------------------------------------------------------------------
-- Transformación a forma normal negativa --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
-- eliminaEquivalencias :: Prop -> Prop
-- tal que (eliminaEquivalencias f) es una fórmula equivalente a f sin
-- signos de equivalencia. Por ejemplo,
-- eliminaEquivalencias (p <--> q)
-- ==> ((p --> q) /\ (q --> p))
-- eliminaEquivalencias ((p <--> q) /\ (q <--> r))
-- ==> (((p --> q) /\ (q --> p)) /\ ((q --> r) /\ (r --> q)))
-- ---------------------------------------------------------------------

eliminaEquivalencias :: Prop -> Prop
eliminaEquivalencias = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
-- eliminaImplicaciones :: Prop -> Prop
-- tal que (eliminaImplicaciones f) es una fórmula equivalente a f sin
-- signos de implicación. Por ejemplo,
-- eliminaImplicaciones (p --> q)
-- ==> (no p \/ q)
-- eliminaImplicaciones (eliminaEquivalencias (p <--> q))
-- ==> ((no p \/ q) /\ (no q \/ p))
-- Nota: Se supone que f no tiene signos de equivalencia.
-- ---------------------------------------------------------------------

eliminaImplicaciones :: Prop -> Prop
eliminaImplicaciones = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
-- interiorizaNegación :: Prop -> Prop
-- tal que (interiorizaNegación f) es una fórmula equivalente a f donde
-- las negaciones se aplican sólo a fórmulas atómicas. Por ejemplo,
-- interiorizaNegación (no (no p)) ==> p
-- interiorizaNegación (no (p /\ q)) ==> (no p \/ no q)
-- interiorizaNegación (no (p \/ q)) ==> (no p /\ no q)
-- interiorizaNegación (no (no (p \/ q))) ==> (p \/ q)
-- interiorizaNegación (no ((no p) \/ q)) ==> (p /\ no q)
-- Nota: Se supone que f no tiene equivalencias ni implicaciones.
-- ---------------------------------------------------------------------

interiorizaNegación :: Prop -> Prop
interiorizaNegación = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
-- formaNormalNegativa :: Prop -> Prop
-- tal que (formaNormalNegativa f) es una fórmula equivalente a f en
-- forma normal negativa. Por ejemplo,
-- formaNormalNegativa (p <--> q)
-- ==> ((no p \/ q) /\ (no q \/ p))
-- formaNormalNegativa ((p \/ (no q)) --> r)
-- ==> ((no p /\ q) \/ r)
-- formaNormalNegativa ((p /\ (q --> r)) --> s)
-- ==> ((no p \/ (q /\ no r)) \/ s)
-- ---------------------------------------------------------------------

formaNormalNegativa :: Prop -> Prop
formaNormalNegativa f = undefined

-- ---------------------------------------------------------------------
-- Literales --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
-- literal :: Prop -> Bool
-- tal que (literal f) se verifica si la fórmula F es un literal. Por
-- ejemplo,
-- literal p ==> True
-- literal (no p) ==> True
-- literal (no (p --> q)) ==> False
-- ---------------------------------------------------------------------

literal :: Prop -> Bool
literal = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir el tipo de dato Literal como sinónimo de
-- fórmula.
-- ---------------------------------------------------------------------

type Literal = Prop

-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
-- complementario :: Literal -> Literal
-- tal que (complementario l) es el complementario de l. Por ejemplo,
-- complementario p ==> no p
-- complementario (no p) ==> p
-- ---------------------------------------------------------------------

complementario :: Literal -> Literal
complementario = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
-- literalesFórmulaFNN :: Prop -> [Literal]
-- tal que (literalesFórmulaFNN f) es el conjunto de los literales de la
-- fórmula en forma normal negativa f.
-- literalesFórmulaFNN (p \/ ((no q) \/ r)) ==> [p,no q,r]
-- literalesFórmulaFNN p ==> [p]
-- literalesFórmulaFNN (no p) ==> [no p]
-- ---------------------------------------------------------------------

literalesFórmulaFNN :: Prop -> [Literal]
literalesFórmulaFNN = undefined

-- ---------------------------------------------------------------------
-- Transformación a forma normal conjuntiva --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
-- interiorizaDisyunción :: Prop -> Prop
-- tal que (interiorizaDisyunción f) es una fórmula equivalente a f
-- donde las disyunciones sólo se aplica a disyunciones o literales. Por
-- ejemplo,
-- interiorizaDisyunción (p \/ (q /\ r)) ==> ((p \/ q) /\ (p \/ r))
-- interiorizaDisyunción ((p /\ q) \/ r) ==> ((p \/ r) /\ (q \/ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaDisyunción :: Prop -> Prop
interiorizaDisyunción = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
-- formaNormalConjuntiva :: Prop -> Prop
-- tal que (formaNormalConjuntiva f) es una fórmula equivalente a f en
-- forma normal conjuntiva. Por ejemplo,
-- formaNormalConjuntiva (p /\ (q --> r))
-- ==> (p /\ (no q \/ r))
-- formaNormalConjuntiva (no (p /\ (q --> r)))
-- ==> ((no p \/ q) /\ (no p \/ no r))
-- formaNormalConjuntiva (no(p <--> r))
-- ==> (((p \/ r) /\ (p \/ no p)) /\ ((no r \/ r) /\ (no r \/ no p)))
-- ---------------------------------------------------------------------

formaNormalConjuntiva :: Prop -> Prop
formaNormalConjuntiva f = undefined

-- ---------------------------------------------------------------------

-- Ejercicio 11.2: validaPorFNC

validaPorFNC:: Prop -> Bool
validaPorFNC = undefined

-- validaPorFNC ((p --> q) \/ (q --> p)) == True
-- validaPorFNC ((p \/ q) /\ ((no q) \/ r)) == False
-- validaPorFNC (p --> p) == True

-- ---------------------------------------------------------------------
-- Transformación a forma normal disyuntiva --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
-- interiorizaConjunción :: Prop -> Prop
-- tal que (interiorizaConjunción f) es una fórmula equivalente a f
-- donde las conjunciones sólo se aplica a conjunciones o literales. Por
-- ejemplo,
-- interiorizaConjunción (p /\ (q \/ r)) ==> ((p /\ q) \/ (p /\ r))
-- interiorizaConjunción ((p \/ q) /\ r) ==> ((p /\ r) \/ (q /\ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------

interiorizaConjunción :: Prop -> Prop
interiorizaConjunción = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
-- formaNormalDisyuntiva :: Prop -> Prop
-- tal que (formaNormalDisyuntiva f) es una fórmula equivalente a f en
-- forma normal disyuntiva. Por ejemplo,
-- formaNormalDisyuntiva (p /\ (q --> r))
-- ==> ((p /\ no q) \/ (p /\ r))
-- formaNormalDisyuntiva (no (p /\ (q --> r)))
-- ==> (no p \/ (q /\ no r))
-- ---------------------------------------------------------------------

formaNormalDisyuntiva :: Prop -> Prop
formaNormalDisyuntiva f = undefined

-- ---------------------------------------------------------------------

-- Ejercicio 13.2: satisfaciblePorFND

satisfaciblePorFND:: Prop -> Bool
satisfaciblePorFND f = undefined

-- satisfaciblePorFND ((p \/ q) /\ ((no q) \/ r)) == True
-- satisfaciblePorFND (p /\ (no p)) == False
-- satisfaciblePorFND ((p --> q) \/ (q --> p)) == True

</source>

Archivo:ResolucionProposicional.hs

2013-05-02T08:55:57Z

Mjoseh:

Archivo:Clausulas.hs

2013-05-02T08:55:41Z

Mjoseh:

Archivo:FormasNormales.hs

2013-05-02T08:55:24Z

Mjoseh:

Lógica matemática y fundamentos

2013-05-02T08:54:48Z

Mjoseh:

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

=== Relaciones de ejercicios ===
* '''Relación 1''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:Rel_2.hs |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Eliminación de conectivas. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Formalización de argumentos en lógica de primer orden. ([[Rel_6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* '''Relación 7''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos proposicionales en Haskell. ([[Media:Rel_8.hs |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]] y [[Relación 11 |Solución colaborativa]]).

=== Teorías Isabelle/HOL de los temas de deducción natural ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].

=== Ejercicios evaluables ===
* '''Ejercicio 1''': [[Ejercicio 1 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Ejercicio 2''': [[Ejercicio 2 |Deducción natural en lógica de primer orden con Isabelle/HOL]].
* '''Nota al ejercicio 2''': los lemas auxiliares que se usen en una demostración por deducción natural han de ser probados de forma no automática. Se amplía el plazo hasta el viernes 3 de mayo para que se envíe el ejercicio 2 teniendo en cuenta esta aclaración.
* '''Ejercicio 3''': [[Ejercicio 3 |Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos]].

=== Problemas semanales ===
* '''Problema 1''': [[Problema 1 | Inducción sobre fórmulas]].
* '''Problema 2''': [[Problema 2 | Subconjuntos inconsistentes]].

E3

2013-04-26T10:44:25Z

Mjoseh: Página creada con '<source lang = "isar"> header {* E3: Argumentación y Deducción natural en lógica de primer orden *} theory E3 imports Main begin text {* Ej. 1: Los perros lobos y los ter...'

<source lang = "isar">

header {* E3: Argumentación y Deducción natural en lógica de primer orden *}

theory E3
imports Main
begin

text {* Ej. 1: Los perros lobos y los terrier son perros cazadores. Los
perros cazadores y los perros falderos son animales domesticados. Los
animales domesticados son mansos y útiles. Algunos perros lobos no son
ni mansos ni pequeños.
(a) Demostrar que algunos terrier son pequeños pero no son mansos.
(b) ¿Seguiría siendo cierta la conclusión si ningún perro lobo fuera
manso?

Simbología: L(x): x es perro lobo, T(x): x es terrier, C(x): x es
cazador, F(x): x es perro faldero, M(x): x es manso, U(x): x es útil,
P(x): x es pequeño, D(x): x es doméstico). *}

text {* Ej. 2: Todo pasajero viaja en primera o en clase turista. Cada
pasajero está en clase turista si y sólo si no es rico. Algunos
pasajeros son ricos. No todos los pasajeros son ricos.
(a) Demostrar que algunos pasajeros viajan en clase turista.
(b) Si ningún pasajero fuera rico, viajaría alguno en primera?.

Simbología: P(x): x es pasajero, T(x): x viaja en clase turista,
Pr(x): x viaja en primera, R(x): x es rico. *}

text {* Ej. 3: Las abejas y las avispas pican si están enojadas o
asustadas.
(a) Luego, cualquier abeja pica si está enojada.
(b) Si hay alguna abeja, ¿es cierto que alguna no pica?

Simbología: Ab(x): x es abeja, Av(x): x es avispa, A(x): x está asustada,
E(x): x está enojada, P(x): x pica. *}

text {* Ej. 4: Cualquier autor tiene éxito si y sólo si es muy
leído. Todos los autores son intelectuales. Algunos autores tiene
éxito pero no son muy leidos.
(a) Demostrar todos los intelectuales son autores.
(b) ¿Seguiría siendo cierta la conclusión si ningún autor tuviera éxito?.

Simbología: A(x): x es autor, E(x): x tiene éxito, L(x): x es muy leído,
I(x): x es intelectual. *}

text {* Ej. 5: Vender un arma no registrada es un crimen. Todas las
armas que posee Rojo se las compró al Zurdo o al Tuerto. Una de las
armas de Rojo es una pistola no registrada. Rojo nunca le compró nada
al Tuerto,
(a) Demostrar que el Zurdo es un criminal.
(b) ¿Es también un criminal el Tuerto?

Simbología: R(x): x está registrada, P(x): x es una pistola,
C(x): x es un criminal, A(x): x es un arma, T(x,y): x posee y,
V(x,y,z): x vendió y a z, r: Rojo, z: el Zurdo, t: el Tuerto. *}

text {* Ej. 6: Todo lo que hay en mi escritorio es una obra
maestra. Quienquiera que escriba una obra maestra es un genio. Alguna
persona desconocida escribió alguna de las novelas que hay en mi
escritorio.
(a) Demostrar que alguna persona desconocida es un genio.
(b) ¿Son genios todas las personas desconocidas?

Simbología: E(x): x está en mi escritorio, M(x): x es una obra
maestra, P(x): x es una persona, G(x): x es un genio, D(x): x es
desconocido, N(x): x es una novela, Es(x,y): x escribió y. *}

text {* Ej. 7: Nadie respeta a una persona que no se respeta a sí
misma. Nadie contratará a una persona que no se respeta.
(a) Demostrar que una persona que no respeta a nadie nunca será
contratada por nadie.
(b) Y, si respeta a alguién, ¿podrá ser contratada?.

Simbología: P(x): x es una persona, R(x,y): x respeta a y,
C(x,y): x contrata a y. *}

text {* Ej. 8: Todo libro que sea aprobado por todos los críticos será leído
por cualquier persona literata. Cualquiera que lea cualquier cosa hablará de
ella. Un crítico aprobará cualquier libro escrito por cualquier persona que
le adule. Los literatos y los críticos son personas. Sólo las personas se
adulan. Nada es a la vez libro y persona.
(a) Demostrar que si alguien adula a todos los críticos, entonces cualquier
libro que escriba será comentado por todas las personas literatas.
(b) ¿Es cierto el recíproco?

Simbología: Li(x): x es libro, Cr(x): x es un crítico, T(x): x es un literato,
P(x): x es una persona, A(x,y): x aprueba y, L(x,y): x lee y, C(x,y): x comenta y,
F(x,y): x adula y, E(x,y): x escribe y. *}

text {* Ej. 9: 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. *}

text {* Ej. 10: Una obra de arte que relata algo puede ser comprendida por
todos. Algunas obras de arte religioso han sido creadas por grandes
artistas. Cualquier obra de arte religioso relata una historia que
inspira. Sólo las personas admiran algo.
(a) Demostrar que si algunas personas sólo admiran lo que no pueden
entender, entonces algunas creaciones de grandes artistas no serán
admiradas por todos.
(b) ¿Es cierto el recíproco?

Simbología: P(x): x es persona, Ar(x): x es un gran artista, H(x): x es
una historia, I(x): x inspira, Re(x): x es religioso, Ob(x): x es una
obra de arte, C(x,y): x crea y, A(x,y): x admira y, R(x,y): x relata y,
E(x,y): x puede entender y. *}

text {* Ej. 11: Si hay genios, entonces todos los grandes compositores son
genios. Si alguien es temperamental, todos los genios son
temperamentales.
(a) Demostrar que si alguien es un genio temperamental, entonces
todos los grandes compositores son temperamentales.
(b) ¿Todos los genios son temperamentales?
(c) ¿Existe algún genio temperamental?

Simbología: G(x): x es un genio, C(x): x es un gran compositor,
P(x): x es una persona, T(x): x es temperamental. *}

text {* Ej. 12: Cualquier hombre de negocios que sea un poeta debe ser
rico. Todos los hombres ricos son conservadores. Si algún conservador no ama
la poesía entonces ningún poeta es conservador.
(a) Demostrar que si hay algún hombre rico que no ama la poesía, entonces
ningún hombre de negocios es poeta.
(b) En el caso de que exista algún hombre rico, ¿alguno no ama la poesía?

Simbología: N(x): x es un honbre de negocios, P(x): x es un poeta, R(x): x
es un hombre rico, C(x): x es un conservador, A(x): x ama la poesía. *}

text {* Ej. 13: Ningún testigo cuerdo mentiría si su mentira lo implicase en un
crimen.
(a) Demostrar que si cualquier testigo se implicara en un crimen,
entonces, si todos los testigos fuesen cuerdos, ese testigo no mintió.
(b) ¿La conclusión sería cierta si sólo alguno de los testigos fuesen cuerdos?

Simbología: C(x): x está cuerdo, T(x): x es un testigo, M(x): x miente, I(x):
x se implica en un crimen. *}

text {* Ej. 14: Si falta una joya, será devuelta si todos los
sirvientes son honestos. Si algún sirviente es honesto, todos lo
son.
(a) Demostrar que si falta alguna joya, entonces si al menos un
sirviente es honesto, será devuelta.
(b) ¿Podemos asegurar que si hay un sirviente deshonesto, la joya no
será devuelta?

Simbología: J(x): x es una joya, F(x): x falta,
S(x): x es un sirviente, H(x): x es honesto,
D(x): x será devuelta. *}

text {* Ej. 15: Quienquiera que apoye a Santi votará por Juan. Andrés no votará
por nadie que no sea amigo de Pedro. Ningún amigo de Félix tiene como amigo a
Juan. La relación de amistad es simétrica.
(a) Demostrar que si Pedro es un amigo de Félix, Andrés no apoyará a Santi.
(b) ¿Es cierto el recíproco?

Simbología: A(x,y): x apoya a y, V(x,y): x vota por y, G(x,y): x es amigo
de y, a: Andrés, s: Santi, j: Juan, p: Pedro, f: Félix. *}

text {* Ej. 16: Cualquier caballo es más veloz que cualquier
perro. Algunos galgos son más veloces que cualquier liebre. Los
galgos son perros. La relación de ser más veloz es transitiva.
(a) Demostrar que cualquier caballo es más veloz que cualquier liebre.
(b) ¿Es cierto que cualquier galgo es más veloz que cualquier liebre?

Simbología: P(x): x es perro, G(x): x es galgo, L(x): x es liebre,
C(x): x es caballo, V(x,y): x es más veloz que y. *}

text {* Ej. 17: Existe un hombre al que todos desprecian.
(a) Demostrar que existe al menos un hombre que se desprecia a sí mismo.
(b) ¿La conclusión sería cierta en el caso de que sólo supiéramos que
existe un hombre al que algunos desprecian?

Simbología: H(x): x es hombre, D(x,y): x desprecia a y. *}

text {* Ej. 18: Cualquiera que haya visitado el edificio ha sido
observado. Todo el que haya observado a Andrés tendría que
recordarle. Nadie recuerda a Andrés.
(a) Demostrar que Andrés no visitó el edificio.
(b) ¿La conclusión sería cierta en el caso de que alguien no
recordara a Andrés?

Simbología: a: Andrés, V(x): x vistó el edificio,
Ob(x,y): x observó a y, R(x,y): x recuerda a y. *}

text {* Ej. 19: Si todas las medicinas están contaminadas, entonces todos los
técnicos negligentes son unos bribones. Si hay medicinas contaminadas,
entonces todas las medicinas están contaminadas y son peligrosas. Todos los
germicidas son medicinas. Sólo los negligentes son distraídos.
(a) Demostrar que si cualquier técnico es distraído y si algunos germicidas
están contaminados, los técnicos son bribones.
(b) ¿Podemos asegurar lo mismo en el caso de que sólo supiéramos que hay
técnicos distraídos?

Simbología: M(x): x es medicina. C(x): x está contaminada,
T(x): x es técnico, N(x): x es un negligente,
B(x): x es un bribón, G(x): x es germicida,
D(x): x es distraído. *}

text {* Ej. 20: Ningún individuo que sea candidato será derrotado si hace una
buena campaña. Todo individuo que se postula es un candidato. Cualquier
candidato que no sea derrotado, será elegido. Todo individuo que sea elegido
hace una buena campaña.
(a) Demostrar que todo individuo que se postula será elegido si y
sólo si hace una buena campaña.
(b) Si algún individuo se postula, ¿habrá candidatos que no sean
elegidos?

Simbología: I(x): x es individuo, C(x): x es candidato,
D(x): x es derrotado, B(x): x hace una buena campaña,
P(x): x se postula, E(x): x es elegido. *}

text {* Ej. 21: Todos los miembros son oficiales y caballerosos. Todos los
oficiales son combatientes. Los caballeros y los no combatientes son
pacifistas. Ningún pacifista es caballero si éste es combatiente. Algunos
miembros son combatientes si y sólo si son oficiales.
(a) Demostrar que no todos los miembros son combatientes.
(b) ¿Podemos asegurar lo mismo en el caso de que no todos los miembros
sean oficiales y caballerosos?

Simbología: M(x): x es miembro, Of(x): x es oficial, C(x): x es caballero,
Co(x): x es combatiente, P(x): x es pacifista. *}

text {* Ej. 22: Si hay liberales, todos los filósofos son liberales. Si hay
humanistas, todos los liberales son humanistas.
(a) Demostrar que si hay humanistas que sean liberales, entonces todos los
filósofos son humanistas.
(b) ¿Todos los liberales son humanistas
(c) ¿Existe algún liberal humanista?

Simbología: L(x): x es liberal, F(x): x es filósofo, H(x): x es humanista. *}

text {* Ej. 23: Si algo se pierde, se sabrá que se ha perdido si cada
cual aprecia sus pertenencias. Si alguien aprecia sus pertenencias,
todos las aprecian.
(a) Demostrar que si algo se pierde, entonces, si alguien aprecia
sus pertenencias, se sabrá que algo se ha perdido.
(b) ¿Podemos asegurar que si alguien no aprecia sus pertenencias,
no se sabrá que algo se ha perdido?

Simbología: P(x): x es una persona, Per(x): x se ha perdido, A(x): x
aprecia sus pertenencias, S(x): se sabrá que x se ha perdido. *}

text {* Ej. 24: Todos los que pertenecen al Club de la Playa tienen
más dinero que cualquier miembro del Club del Campo. No todos los
miembros del cub de la Playa tiene más dinero que cualquiera que no
pertenezca al mismo.
(a) Demostrar que no todos pertenecen a alguno de los dos clubes.
(b) ¿Es cierto que hay algún miembro del Club de la Playa que tiene
más dinero que algún miembro del Club del campo?

Simbología: P(x): x es una persona, CP(x): x pertenece al club de
la playa, CC(x): x pertenece al Club del campo, D(x,y): x tiene más
dinero que y. *}

text {* Ej. 25: Quien ama apasionadamente acaba siendo desgraciado;
quienes no pueden ocultar su pasión mueren prematuramente.
(a) Demostrar que si todos aquellos que acaban siendo desgraciados no
pueden ocultar su pasión, entonces, todos aquellos que amen de
forma apasionada mueren prematuramente.
(b) ¿Es cierto el recíproco?

Simbologia: A(x): x ama, P(x): x es apasionado, D(x): x es desgraciado,
Oc(x): x oculta la pasión, M(x): x muere prematuramente.
*}

text {* Ej. 26: Cualquier automóvil que tenga buenos frenos es seguro para el
conductor y seguro para los pasajeros.
(a) Demostrar que si un automóvil es nuevo, entonces, si todos los
automóviles nuevos tienen buenos frenos, es seguro para el conductor.
(b) ¿Podemos asegurar que todos los automóviles nuevos son seguros para
los pasajeros?

Simbología: A(x): x es un automóvil, F(x): x tiene buenos frenos,
C(x): x es seguro para el conductor, P(x): x es seguro para los pasajeros,
N(x): x es nuevo. *}

text {* Ej. 27: Todo ejecutivo que sea poeta es un hombre
imaginativo. Todo hombre imaginativo es amante del riesgo. Si todo
amante del riesgo no es poeta, entonces, ningún poeta es amante del
riesgo.
(a) Demostrar que si todo hombre imaginativo no es poeta, entonces,
ningún ejecutivo es poeta.
(b) ¿Es cierto el recíproco?

Simbología: E(x): x es ejecutivo, P(x): x es poeta, I(x): x es imaginativo,
R(x): x es amante del riesgo. *}

text {* Ej. 28: Las substancias radioactivas tienen vida corta o un
valor medicinal. Ningún isótopo de Uranio que sea radioactivo tiene
una vida corta.
(a) Demostrar que si todos los isótopos de uranio son radioactivos,
entonces, todos los isótopos de uranio tienen un valor medicinal.
(b) ¿Es cierto el recíproco?

Simbología: R(x): x es sustancia radioactiva, C(x): x tiene una vida
corta, M(x): x tiene valor medicinal, I(x): x es isótopo del Uranio. *}

end
</source>