Gestión Mecanizada del conocimiento matemático

Este proyecto nace de la confluencia de dos líneas de investigación desarrolladas a lo largo de los años por dos equipos distintos, uno de La Rioja y otro de Sevilla. El equipo de La Rioja ha trabajado en los aspectos computacionales de la Topología Algebraica, y el de Sevilla en Lógica. Este proyecto servirá para unificar estas líneas dentro del área conocida como Gestión del Conocimiento Matemático (MKM, según sus siglas en inglés). Dicha área pretende integrar todos los aspectos de la mecanización de las matemáticas, incluyendo el cálculo (álgebra computacional), la deducción (razonamiento y verificación) y la comunicación (vía lenguajes basados en XML). Todos estos aspectos serán tratados para algunas partes de la Topología Algebraica. Los relativos a la deducción y la comunicación serán también abordados para la Lógica. Además, técnicas de la Lógica Computacional (como los sistemas de rescritura) serán empleadas para la formalización en Topología Simplicial. Más concretamente, trabajos realizados por el grupo de Sevilla con el demostrador mecanizado ACL2 serán aplicados a la formalización y verificación de algoritmos que aparecen en los sistemas de cálculo simbólico en Topología desarrollados por el grupo de La Rioja.