En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección d un compilador de expresiones aritméticas.
La clase se ha basado en la siguiente teoría Isabelle
Read More “RA2011: Demostracción en Isabelle de la corrección de un compilador”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha ampliado el estudio de las demostraciones por inducción en Isabelle. Se ha estudiados:
La clase se ha basado en la siguiente teoría Isabelle
Read More “RA2011: Demostraciones por inducción en Isabelle”
En la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se ha presentado una introducción a la lógica matemática basada en la Introduction to Mathematical Logic de Valentin Goranko.
En la introducción se hace un recorrido por la historia de la lógica matemática resaltando los problemas, métodos y aplicaciones. Se consideran los siguientes períodos:
En segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los 6 primeros ejercicios de la 16ª relación.
El objetivo de esta relación es estudiar la generación y el número de
las principales operaciones de la combinatoria. En concreto, se
estudia
Además, se estudia dos temas relacionados:
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2011: Combinatoria en Haskell (1)”
En primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la 16ª relación sobre ejercicios de exámenes del curso 2010-11 correspondientes a los 9 primeros temas del curso.
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2011: Ejercicios de exámenes del curso 2010-11”