CSL (Computer Science Logic) es el congreso anual de la EACSL (European Association for Computer Science Logic). El tema fundamental del congreso es la interrelación entre lógica y computación.
El CSL 2010 se celebrará en Brno (República Checa) el 23 de Agosto. El plazo de envío termina el 26 de marzo.
Una de las líneas de desarrollo de la Lógica Computacional es abordar formalizaciones de resultados matemáticos complejos. El intento de formalización produce como efectos laterales la formalización del conocimiento implícito en el resultado (el mathware) y el desarrollo de nuevos procedimientos de decisión.
Uno de los grandes retos actuales es la formalización de la demostración de Andrew Wiles del último teorema de Fermat. Una descripción detallada del reto se encuentra en el artículo Computer verification of Wiles’ proof of Fermat’s Last Theorem de Wim H. Hesselink. En el artículo se traza la hoja de ruta de la formalización describiendo la estructura de la demostración de Wiles. Una de las principales dificultades radica en comentando la necesidad de disponer de sistemas de razonamiento que incorporen cálculo simbólico. Hesselink estima que se tardarán unos 50 años en conseguirse la formalización del teorema de Wiles.
El inicio del primer trabajo sobre la automatización del razonamiento. Los trabajos realizados desde entonces se encuentran en las páginas de publicaciones, tesis y trabajos de investigación dirigidos y cursos impartidos. La ordenación de estas páginas es simplemente cronológica. Una visión más ordenada del trabajo desarrollado durante estos años se encuentra en las transparencias de las conferencias que dí en la Universidad de La Coruña: Un viaje a través del razonamiento automático (Experiencias del GLC de la US). En ella se describen los sistemas de razonamiento que hemos utilizado y las teorías que hemos formalizado.
Hoy, 1 de enero de 2010, empieza la andadura de Vestigium. En esta presentación intentaré responder las siguientes cuestiones
He creado el blog, fundamentalmente, para complementar los medios de comunicación del Grupo de Lógica Computacional de la Universidad de Sevilla. El medio tradicional ha sido el Seminario de Lógica Computacional. Recientemente se ha creado una lista de correo del Grupo. Dado que el conocimiento es difícil de gestionar en las listas de correo he empezado el blog para facilitar la gestión del conocimiento.
He elegido Vestigium como nombre del blog por la etimología de investigar
La palabra ”’investigar”’ viene del latín ”investigare”, la cual deriva de ”’vestigium”’ que significa en “pos de la huella de”, es decir “ir en busca de una pista”.
Detrás del nombre se esconde la segunda, y no por ello menos importante, razón para crear el blog: dejar una traza de los trabajos realizados en Lógica Computacional por nuestro grupo y de los trabajos ajenos relacionados con los nuestros. Es decir, investigar en Lógica Computacional.
Hablando de investigación, terminaré la presentación del blog con una cita de uno de los libros de texto que estudié en Selectivo de Ciencias. En la introducción de Geometría vectorial (ed. Alhambra, 1968), Norberto Cuesta Dutari, observa que:
Aprender lo que ignoramos, enseñados de quien lo sabe, e inventar lo que nadie nos puede enseñar, son actividades mentales isomorfas, y ambas tan importantes como complicadas.