Exploración automática de teorías matemáticas

PorJosé A. Alonso

La exploración automática de teorías matemáticas es un tema emergente de investigación dentro de la Lógica Computacional. Su objetivo es desarrollar sistemas informáticos que ayuden en el desarrollo automático de teorías matemáticas, incluyendo la invención de definiciones, teoremas, conjeturas, problemas, ejemplos y algoritmos,

El primer congreso sobre exploración de teorías matemáticas fue el Automatheo 2009 y se celebró en Linz, Austria.

El segundo congreso sobre exploración de teorías matemáticas es el Automatheo 2010 y se celebrará en Edimburgo el 14 y 15 de Julio de 2010. La fecha de envío de comunicaciones finaliza el 2 de Junio.

Trabajo de Lógica Computacional en Edimburgo

PorJosé A. Alonso

Se ha ofertado una plaza para realizar una tesis doctoral sobre lógica computacional en la Universidad de Edimburgo.

La tesis se inscribe dentro del proyecto AI4FM (the use of AI to automate proof search in Formal Methods). El objetivo del proyecto es aplicar técnicas de IA, fundamentalmente aprendizaje automático, para automatizar las demostraciones de las obligaciones de pruebas generadas por los sistemas de razonamiento.

El tema de la tesis es The Productive Use of Failure in Formal Methods y será dirigida por Alan Bundy.