I1M2012: Razonamiento sobre programas Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo demostrar propiedades de funciones definidas en Haskell. Los esquemas de demostración estudiados son:

  • por simplificación,
  • por casos,
  • por inducción sobre los números naturales,
  • por inducción sobre listas,
  • por inducción anidada y
  • por generalización e inducción.

Las transparencias usadas en la clase son las del tema 8:
Read More “I1M2012: Razonamiento sobre programas Haskell”

LMF2013: Introducción a la programación lógica con Prolog

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha realizado una introducción a la programación lógica con Prolog como aplicación de la resolución en la lógica de primer orden.

Se ha presentado el sistema deductivo de Prolog en tres fases: proposicional, relacional y funcional. En cada una se ha comentado cómo representar el conocimiento, cómo realizar consultas y cómo es el razonamiento de Prolog para calcular las respuestas.

Los apuntes de esta clase son Introducción a la programación lógica con Prolog (páginas 1-26).

Las transparencias de esta clase son las páginas 1 a 18 del tema 13
Read More “LMF2013: Introducción a la programación lógica con Prolog”

Reseña: The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre la demostración del teorema de Jordan-Hölder para grupos finitos titulado The rooster and the butterflies.

Su autora es Assia Mahboubi (de Microsoft Research – Inria Joint Centre).

El trabajo se presentará en julio en el CICM 2013 (Conferences on Intelligent Computer Mathematics).

Su resumen es

This paper describes a machine-checked proof of the Jordan-Hölder theorem for finite groups. This purpose of this description is to discuss the representation of the elementary concepts of finite group theory inside type theory. The design choices underlying these representations were crucial to the successful formalization of a complete proof of the Odd Order Theorem with the Coq system.