I1M2012: Ejercicios de evaluación perezosa y listas infinitas (2)

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentando soluciones de ejercicios sobre evaluación perezosa y listas infinitas de las relación 17.

En los comentarios se ha resaltado

  • en los ejercicios 2 y 3:
    • la importancia del orden de las condiciones en las definiciones de listas por comprensión,
    • la eficiencia del cálculo sobre la búsqueda.
  • en el ejecicio 6.2 el uso de iterate y
  • en la definición de los números triangulares el uso de scanl.

Los ejercicios, y sus soluciones, se muestran a continuación
Read More “I1M2012: Ejercicios de evaluación perezosa y listas infinitas (2)”

LMF2013: Deducción natural proposicional en Isabelle/HOL

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

Para cada uno de los ejemplos se ha presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y 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”