El curso Informática (de 1º de Grado en Matemáticas) comienza el martes 24 de septiembre.
Las clases son los martes y viernes de 12:00 a 14:00 en el aula EC03 de la Facultad de Matemáticas.
Las clases terminan el 6 de junio de 2014.
Se ha publicado un artículo sobre razonamiento formalizado en topología algebraica titutado On the role of formalization in computational mathematics.
Su autor es Julio Rubio (de la Universidad de la Rioja).
Su resumen es
In this paper, we will report on the developments carried out in Isabelle/HOL, ACL2 and Coq/SSReflect on Computational Algebraic Topology, in the frame of the ForMath European project. The aim is to illustrate, trough concrete examples, the role of formalization technologies in Computational Mathematics in general.
En las Olimpiadas de Matemáticas del 2001 se propuso el siguiente problema
Buscar todas las sucesiones finitas (x(0), x(1),…,x(n)) tales que para todo j, 0 ≤ j ≤ n, x(j) es igual al número de veces que aparece j en la sucesión.
Las sucesiones que cumplen la anterior condición se llaman auto descriptivas. Un ejemplo de sucesión auto descriptiva es [5,2,1,0,0,1,0,0,0] ya que
En la siguiente relación de ejercicios, elaborada para la asignatura de Informática (de 1º del Grado en Matemáticas) y para la siguiente versión del libro Piensa en Haskell, se resuelve el problema con Haskell.
Read More “Sucesiones auto descriptivas en Haskell”
El viernes pasado, John D. Cook escribió el artículo Ramanujan’s nested radical en el que comenta el siguiente problema planteado por Ramanujan en el Journal of Indian Mathematical Society:
¿Cuál es el valor de la siguiente expresión?
A partir del problema he elaborado la siguiente relación de ejercicios en Haskell para la asignatura de Informática (de 1º del Grado en Matemáticas).
Read More “Problema de Ramanujan de radicales anidados”
Se ha publicado un artículo sobre automatización del razonamiento titulado Theory exploration for interactive theorem proving.
Su autora es Moa Johansson (de la Universidad Técnica Chalmers en Gotemburgo, Suecia).
Su resumen es
Theory exploration is an automated reasoning technique for discovering and proving interesting properties about some set of given functions, constants and datatypes. In this note we describe ongoing work on integrating the HipSpec theory exploration system with the interactive prover Isabelle. We believe that such an integration would be beneficial for several reasons. In an interactive proof attempt a natural application would be to allow the user to ask for some suggestions of new lemmas that might help the current proof development. Theory exploration may also be used to automatically generate and prove some basic lemmas as a first step in a new theory development. Furthermore, when the theory exploration system is used as a stand-alone system, it should output a checkable proofs, for instance for Isabelle, so that sessions can be saved for future use.
El trabajo se presentó el 22 de julio en el AI4FM 2013 (4th International Workshop on Artifical Intelligence for Formal Methods).