Tesis doctoral de Inmaculada Medina Bulo
En este trabajo se han desarrollado los elementos necesarios para especificar, implementar y verificar la correción del algoritmo de buchberger para el cálculo de bases de grí¶bner, utilizando para ello un sistema de razonamiento automatizado (acl2); esto incluye la formalización completa y precisa de toda la teoría matemática subyacente. Concretamente: -el desarrollo de una teoría computacional sobre los anillos de polinomios de múltiples variables. -la obtención de un orden natural a los polinomios de múltiples variables y demostración de su buena fundamentación. -la representación de los conceptos asociados a los ideales polinómicos de manera que sea posible razonar sobre ellos de manera automatizada. -el desarrollo de una teoría computacional sobre las reducciones polinómicas estableciendo su relación con las reduccines abstractas. -la representación de los conceptos asociados a las bases de grí¶bner de manera que sea posible razonar sobre ellos de manera automatizada. -la implementación del algoritmo de buchberger, especificar sus propiedades y demostrar su corrección. -la obtención de un procedimiento de decisión verificado para el problema de la pertenencia al ideal.
Datos académicos de la tesis doctoral «Verificación formal en acl2 del algoritmo de buchberger«
- Título de la tesis: Verificación formal en acl2 del algoritmo de buchberger
- Autor: Inmaculada Medina Bulo
- Universidad: Sevilla
- Fecha de lectura de la tesis: 18/11/2003
Dirección y tribunal
- Director de la tesis
- José Antonio Alonso Jimenez
- Tribunal
- Presidente del tribunal: Luis María Laita de la rica
- agustín Riscos fernández (vocal)
- eugenio Roanes lozano (vocal)
- julio Jesús Rubio García (vocal)