Centenario del Principia Mathematica

Con motivo del centenarario de la publicación del primer volumen del Principia Mathematica de Alfred North Whitehead y Bertrand Russell se está publicando distintos artículos conmemorativos.

Hace dos semanas, El País publicó el artículo de José Manuel Sánchez Ron El valor del fracaso digno.

En el artículo se que comenta que aunque el Principia Mathematica de Whithead y Russell no conseguió su fin (reducir la metemática a la lógica) en cambio, por lo riguroso de sus análisis lógicos y la ambiciosa meta que perseguía, se convirtió en una referencia obligada de toda la lógica y la filosofía de la matemática posteriores. En el artículo recuerda la que le escribión de Alice Mary Hilton a Russell: “Estoy segura de que Principia Mathematica no será olvidado mientras exista una civilización que conserve los trabajos de las mentes realmente grandes”. El artículo termina reflexionando sobre los fines y los medios

No hay que esforzarse mucho en argumentar que poner los fines por encima de los medios constituye una perversión que puede destruir una sociedad. Tal vez sí que haya que detenerse más en señalar que el éxito en una empresa no es siempre lo único que se recuerda. También recordamos, debemos recordar, a los que se esforzaron en empresas exigentes. Aunque fracasasen. Como Whitehead y Russell en Principia Mathematica.

Hace unos días se ha publicado un nuevo artículo conmemorativo:
100 Years Since Principia Mathematica, escrito Stephen Wolfram (el autor del sistema de cálculo simbólico Mathematica y del sistema de búsqueda Wolfram Alpha).

El artículo comienza con un comentario sobre un objetivo compartido por los Principia Mathematica y Mathematica: la formalización de las matemáticas. Realiza un recorrido histórico sobre la formalización de la matemática hasta la publicación de los Principia Mathematica. Compara los avances realizados desde los Principia Mathematica en el razonamiento y en el cálculo simbólico:

In the hundred years since Principia Mathematica, there has been slow progress in presenting theorems of mathematics in formal ways. But the idea of mathematical computation has taken off spectacularly — and has transformed the use of mathematics, and many areas of its development.

El artículo termina con una visión del futuro

In the future, however, I suspect that there will be another level of automation. Probably it will take much less than a hundred years, but in time it will become commonplace not just to make computations to order, but to make to order the very systems on which those computations are based—in effect in the blink of an eye inventing and developing something like a whole Principia Mathematica to respond to some particular purpose.

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

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)

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.

Libro de introducción al cálculo simbólico con Maxima

He aprovechado los primeros días no laborables para recopilar el material sobre cálculo simbólico en Maxima que he usado en las asignaturas Informática de 1º de Matemáticas) y Sofware libre para la enseñanza y aprendizaje de las Matemáticas. Fruto de dicha recopilación es el libro Introducción a Maxima.

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 primera versión del libro y he incluido también las soluciones de los ejercicios propuestos. Espero vuestros comentarios para las siguientes versiones.

Reanudación

Después de 4 meses, reanudo la escritura en Vestigium. Como uno de sus objetivos era servir de diario de las publicaciones en mi sitio en la Red, voy a resumir las realizadas desde la anterior entrada en Vestigium.

He publicado una introducción al sistema de cálculo simbólico Maxima que he usado en las asignaturas de I1M (Informática de 1º de Matemáticas) como en la de SLEAM (Sofware libre para la enseñanza y aprendizaje de las Matemáticas). Los temas y ejercicios publicados son los siguientes:

las relaciones de ejercicios:

Además, en I1M (Informática de 1º de Matemáticas) he publicado dos nuevos temas sobre diseño de algoritmos con Haskell:

En la página de publicaciones he añadido las dos más recientes:

Finalmente, en la wiki del Grupo de Lógica Computacional he añadido las formalizaciones de teorías en PVS: