I1M2012: Comienzo del curso
Las clases del curso Informática (de 1º de Grado en Matemáticas) comenzarán el lunes 1 de octubre.
Reseña: A formal proof of Sasaki-Murao algorithm
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
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)
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:
- la página de la asignatura,
- las transparencias de los temas,
- el libro con los apuntes de los temas,
- el libro sobre la construcción lógica de sistemas lógicos,
- el libro con los enunciados de los ejercicios,
- el libro de exámenes resueltos de cursos anteriores
- el libro de ejercicios de formalización,
- el libro de soluciones de los ejercicios de deducción natural proposicional y
- el libro de soluciones de los ejercicios de deducción natural en lógica de primer orden.
- el libro con los apuntes de los temas,
Reseña: Computing persistent homology within Coq/SSReflect
Se ha publicado un nuevo trabajo de razonamiento formalizado en Coq titulado Computing persistent homology within Coq/SSReflect.
Sus autores son Jónathan Heras, Thierry Coquand, Anders Mörtbeg y Vincent Siles.
Su resumen es
Persistent homology is one of the most active branches of Computational Algebraic Topology with applications in several contexts such as optical character recognition or analysis of point cloud data. In this paper, we report on the formal development of certified programs to compute persistent Betti numbers, an instrumental tool of persistent homology, using the Coq proof assistant together with the SSReflect extension. To this aim it has been necessary to formalize the underlying mathematical theory of these algorithms. This is another example showing that interactive theorem provers have reached a point where they are mature enough to tackle the formalization of nontrivial mathematical theories.
Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.