LMF2013: Deducción natural proposicional en Isabelle/HOL (2)

En la clase de hoy del curso Lógica matemática y fundamentos se ha completado el estudio de la formalización en Isabelle/HOL de las demostraciones por deducción natural estudiadas en el tema 2 que empezamos en la clase anterior.

Para cada uno de los ejemplos se ha presentado distintas demostraciones: desde la detallada (que sea parecida a la mostrada en las transparencias) hasta la automática.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2013: Deducción natural proposicional en Isabelle/HOL (2)”

I1M2012: Ejercicios con tipos de datos algebraicos en Haskell

En las clases de ayer y hoy de Informática de 1º del Grado en Matemáticas hemos comentando soluciones de los ejercicios sobre tipos de datos algebraicos en Haskell de la relaciones 18 y 19.

En la relación 18 se consideran abreviaturas y dos tipos de datos
algebraicos: los números naturales (para los que se define su
producto) y los árboles binarios, para los que se definen funciones
para calcular:

  • los puntos más cercanos,
  • la ocurrencia de un elemento en el árbol,
  • el número de hojas,
  • el carácter balanceado de un árbol y
  • el árbol balanceado correspondiente a una lista.

En la relación 19 se plantean ejercicios sobre árboles binarios. En
concreto, se definen funciones para calcular:

  • el número de hojas de un árbol,
  • el número de nodos de un árbol,
  • la profundidad de un árbol,
  • el recorrido preorden de un árbol,
  • el recorrido postorden de un árbol,
  • el recorrido preorden de forma iterativa,
  • la imagen especular de un árbol,
  • el subárbol de profundidad dada,
  • el árbol infinito generado con un elemento y
  • el árbol de profundidad dada cuyos nodos son iguales a un elemento.

Los ejercicios, y sus soluciones, se muestran a continuación. Los de la relación 18 son
Read More “I1M2012: Ejercicios con tipos de datos algebraicos en Haskell”