RA2012: Introducción a la demostración asistida con Isabelle/HOL

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha presentado:

El ejemplo que se ha visto para introducir los elementos del lenguaje de demostración es el siguiente
Read More “RA2012: Introducción a la demostración asistida con Isabelle/HOL”

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

PorJosé A. Alonso

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

  • 8. Menor número triangular con más de n divisores.
  • 9. Números primos consecutivos con dígitos con igual media.
  • 10. Decisión de pertenencia al rango de una función creciente
  • 11. Pares ordenados por posición.
  • 12. Aplicación iterada de una función.
  • 13. La bicicleta de Turing.
  • 14. La sucesión de Golomb.

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

Reseña: The Picard algorithm for ordinary differential equations in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre ecuaciones diferenciales titulado The Picard algorithm for ordinary differential equations in Coq.

Sus autores son Evgeny Makarov and Bas Spitters (de la Universidad de Nimega, Países Bajos).

Su resumen es

Ordinary Differential Equations (ODEs) are ubiquitous in physical applications of mathematics. The Picard-Lindelöf theorem is the first fundamental theorem in the theory of ODEs. It allows one to solve differential equations numerically. We provide a constructive development of the Picard-Lindelöf theorem which includes a program together with sufficient conditions for its correctness. The proof/program is written in the Coq proof assistant and uses the implementation of efficient real numbers from the CoRN library and the MathClasses library. Our proof makes heavy use of operators and functionals, functions on spaces of functions. This is faithful to the usual mathematical description, but a novel level of abstraction for certified exact real computation.

Las teorías desarrolladas se encuentran aquí.

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

PorJosé A. Alonso

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

PorJosé A. Alonso

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”