En clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentando las soluciones los 6 primeros ejercicios de evaluación perezosa y listas infinitas de la 11ª relación
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2019: Ejercicios de evaluación perezosa y listas infinitas en Haskell”
En la clase de hoy del curso de Razonamiento automático se ha comenzado la presentación de la deducción natural con Isabelle/HOL.
La presentación se basa en los ejemplos del tema 2 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).
La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.
Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la penúltima que es automática y la última es aplicativa.
A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2019: Deducción natural proposicional con Isabelle/HOL (1)”
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han comentado los problemas propuestos en Exercitium del 22 al 29 de noviembre. Los enlaces a dichos problemas, y a sus soluciones, son
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la evaluación perezosa en Haskell. Se han visto la estrategias de evaluación perezosa e impaciente, se han comparado respecto de la terminación y el número de pasos necesarios en las computaciones, se ha aplicado a la computación con estructuras infinitas y se han visto casos en los que se aumenta la eficiencia con evaluación estricta.
Como ejemplo, se ha estudiado el cálculo de los números primos mediante la criba de Erastótenes.
Los apuntes correspondientes a la clase son
Una versión interactiva de los apuntes en IHaskell se encuentra aquí.
En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 4ª relación de ejercicios de cuantificadores sobre listas. Para cada propiedad se dan tres demostraciones en Isabelle/HOL: la primera automática, la segunda estructurada y la tercera totalmente detallada mostrando todos los lemas de HOL que se utilizan en cada paso.
La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2019: Ejercicios de cuantificadores sobre listas en Isabelle/HOL”