En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.
En la presentación se han usado los ejemplos del tema 8 del curso de Informática (de 1º del Grado en Matemáticas).
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Razonamiento sobre programas con Isabelle/HOL (1)”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha presentado la programación funcional en Isabelle/HOL.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Programación funcional con Isabelle/HOL”
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han resueltolos 5 primeros ejercicios de la relación 24. El objetivo de esta relación es ampliar el conjunto de operaciones
sobre polinomios definidas utilizando las implementaciones del TAD de
polinomio estudiadas en el tema 21. Además, en algunos ejemplos de usan polinomios con coeficientes racionales. En Haskell, el número racional x/y se representa por x%y. El TAD de los números racionales está definido en el módulo Data.Ratio.
En los ejercicios se usan las siguientes librerías, estudiadas en el tema 21,
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Operaciones con el TAD de los polinomios en Haskell (1)”
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha completado las soluciones de los ejercicios de la relación 22 que se empezó en la clase de la semana pasada.
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 “I1M2012: Combinatoria en Haskell (2)”
Se ha publicado un artículo de razonamiento formalizado a la economía titulado ForMaRE – formal mathematical reasoning in economics.
Sus autores son Manfred Kerber, Christoph Lange y Colin Rowat (de la Universidad de Birmingham) y lo presentarán hoy en el ARW2013 (20th Automated Reasoning Workshop).
Su resumen es
We present the ForMaRE project which applies FORmal MAthematical REasoning to economics. Theoretical economics makes use of mathematical proof and we seek to increase confidence in these theoretical results by applying formal mathematical reasoning. This will lead on the one hand to new challenge problems in formal reasoning. On the other hand we are conducting research that connects economics and formal methods. We will discuss some areas of interest such as game theory and auctions, where we are currently building a toolbox of formalizations.