Repositorio de producción científica de la Universidad de Sevilla

Verificación formal en ACL2 del Algoritmo de Buchberger

Opened Access Verificación formal en ACL2 del Algoritmo de Buchberger
Estadísticas
Icon
Exportar a
Autor: Medina Bulo, Inmaculada
Director: Alonso Jiménez, José Antonio
Ruiz-Reina, José-Luis
Departamento: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Fecha: 2003-12-18
Tipo de documento: Tesis Doctoral
Resumen: 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 impl...
[Ver más]

Acceder al texto completo

URI: http://hdl.handle.net/11441/36956

Mostrar el registro completo del ítem


Esta obra está bajo una Licencia Creative Commons Atribución-NoComercial-SinDerivadas 4.0 España

Este registro aparece en las siguientes colecciones