I1M2012: Presentación del curso de “Informática (de 1º de Matemáticas)

PorJosé A. Alonso

En la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se ha presentado la asignatura siguiendo el resumen del proyecto docente y los materiales en la página de la asignatura:

Se ha explicado cómo instalar los sistemas y se ha mostrado una sesión sobre el uso de Haskell y emacs. La sesión está grabada en este vídeo.

Se ha comentado el sistema de evaluación y se ha anunciado las fechas de los exámenes de todo el curso.

Reseña: A formal proof of Sasaki-Murao algorithm

PorJosé A. Alonso

La semana pasada se presentó en el MAP2012 (Mathematics, Algorithms and Proofs 2012) un trabajo de aplicación de bibliotecas de razonamiento formalizado en Coq a la verificación de un algoritmo de álgebra computacional.

El título del trabajo es A formal proof of Sasaki-Murao algorithm y sus autores son Tierry Coquand, Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).

El resumen del trabajo es

The Sasaki-Murao algorithm computes the determinant of any square matrix over a commutative ring in polynomial time. The algorithm itself can be written as a short and simple functional program, but its correctness involves non-trivial mathematics. We here represent this algorithm in Type Theory with a new correctness proof, using the Coq proof assistant and the SSReflect extension.

El código Coq de la formalización se encuentra aquí y las transparencias de la presentación se encuentran aquí.

Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.

LI2012: Lógica y programación

PorJosé A. Alonso

En la primera parte de la clase de hoy Lógica Informática se ha comentado las relaciones entre la lógica y la programación. Se han mostrado un programa con una máquina de Turing, un programa en Prolog y un demostrador proposicional en Haskell.

En la segunda parte he comentando relaciones entre las lógicas e informática:

  • la de primer orden con la programación lógica (que verán en la signatura de “Programación declarativa”),
  • la de orden superior con la verificación de sistemas (que verán en la asignatura de “Razonamiento asistido por computador”),
  • las modales con los agentes inteligentes (que verán en la asignatura de “Sistemas inteligentes”)
  • las descriptivas con la Web semántica (que verá en la asignatura de “Representación del conocimiento en la Web”).

LI2012: Presentación del curso de “Lógica informática” (2012-13)

PorJosé A. Alonso

En la clase de hoy, se ha realizado la presentación del curso Lógica Informática siguiendo el plan de la asignatura. Se ha comentado el contenido de la asignatura, el sistema de evaluación y los materiales de la asignatura en la Red: