Curso de Informática (del Grado en Matemáticas)

PorJosé A. Alonso

Como he comentado en otras entradas, uno de los objetivos de este blog es servir de diario de las publicaciones docentes que realizo en mi página personal.

Esta semana he publicado el curso Informática del Grado en Matemáticas (2010-11) que se impartirá desde el 4 de Octubre al 10 de Junio de 2011.

El material del curso publicado hasta ahora está englobado en los siguientes libros:

A lo largo del curso se irán ampliando con los ejercicios, los exámenes y los apuntes de los temas restantes.

Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases

PorJosé A. Alonso

Se ha publicado recientemente el artículo Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases.

En el artículo se presenta una forma de combinar sistemas SAT (basados en el algoritmo DPLL) y bases de Gröbner de forma que cuando se encuentran conflictos, el aprendizaje de las nuevas cláusulas se realice mediante bases de Gröbner en lugar de hacerlo por resolución.

Para experimentar la propuesta, han creado el sistema MiniSat+GB en el que integran el sistema MiniSat con la librería para el cálculo de bases de Gröbner del sistema de cálculo simbólico Reduce.

En los resultados de los experimentos se observa cómo MiniSat+GB supera en eficiencia a MiniSat en los casos en los que se requiere más tiempo de cómputo.

Los autores del artículo son Christoph Zengler y Wolfgang Küchlin que son miembros del Grupo de cálculo simbólico de la Universidad de Tubinga (Tübingen en alemán), Alemania.

El artículo se ha publicado en el LNCS 6244: Computer Algebra in Scientific Computing. (12th International Workshop, CASC 2010)

Libro de introducción al cálculo simbólico con Maxima (versión 2)

PorJosé A. Alonso

En una entrada anterior anuncié la publicación de la primera versión de un libro de introducción al cálculo simbólico con Maxima.

He publicado una nueva versión del libro en la que he eliminado erratas e incluidos los comentarios recibidos.

Esta nueva versión es la que usaré este curso en la asignatura de Informática de 1º de Matemáticas.

En el libro se hace una presentación de Maxima a través de ejercicios resueltos (que se comentan en clases) y propuestos (para resolver por los alumnos en la wiki de la asignatura y, posteriormente, comentar as soluciones en clase).

Esta es la segunda versión del libro y he incluido también las soluciones de los ejercicios propuestos. Espero vuestros comentarios para las siguientes versiones.

Trabajo de lógica computacional en Kassel

PorJosé A. Alonso

El Grupo de Métodos Formales y Verificación de la Universidad de Kassel, Alemania, ha publicado el anuncio de la oferta de una plaza postdoctoral para trabajar en lógica computacional.

El trabajo se desarrollará en el proyecto ERC Model Checking Unleashed.

El objetivo del trabajo es el estudio de aplicaciones no estándard de las técnicas de verificación de modelos (en inglés, model checking) en varias áreas de ciencias de la verificación y temas relacionados.

Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

PorJosé A. Alonso

Se ha publicado un nuevo artículo de formalización: Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

Los autores del artículo son Freek Verbeek y Julien Schmaltz de la Universiad de Radboud en Nimega (en neerlandés: Nijmegen), Paises Bajos.

El artículo se publicó ayer (18 de Septiembre de 2010) en el Journal of Automated Reasoning.

Una versión preliminar del artículo puede leerse aquí y el código ACL2 correspondiente puede obtenerse aquí

El artículo es una demostración en ACL2 de una condición necesaria y suficiente para enrutamiento sin estancamiento introducida por William J. Dally y Charles L. Seitz en su artículo Deadlock Free Message Routing in Multiprocessor Interconnection Networks de 1987.
Read More “Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks”