Tesis doctoral de Gilberto Pérez Vega
En primer lugar, se aborda, de forma ajustada a lo que se va a necesitar, las nociones más prácticas del sistema coq que son necesarias para comprender la formalización de la teoría matemática de los polinomios, su reducción y bases de grí¶bner. el trabajo específico comienza con la formalización de los términos de «n» variables, así como las operaciones más usuales de polinomios en el sistema coq. Se implementa el orden lexicográfico profundizado en la prueba de que dicho orden es bien fundado. para formalizar el anillo de polinomios en varias variables, se describen las pruebas de la estructura de cuerpo abstracto. se implementan los polinomios y los polinomios canónicos, formalizando una igualdad explícita de polinomios original, describiendo también sus operaciones. Se implementa el orden de polinomios demostrando que es noetheriano.Asimismo, se implementa el concepto de ideal. se generaliza, en el sistema de coq, el algoritmo de la división de polinomios en varias variables. Una vez implementada dicha división, llamada reducción; se estudia la relación entre congruencia y reducción, obteniéndose la forma normal módulo un conjunto de polinomios. finalmente, se introduce el concepto de base de grí¶bner, estudiando y probando su equiValencia con otras caracterizaciones alternativas. Para resolver estas equiValencias se da una versión del lema de newman, implementando un esquema de recursión sobre polinomios canónicos, así como propiedades de la confluencia de la reducción.
Datos académicos de la tesis doctoral «Bases de gÁ¶bner: desarrollo formal en coq«
- Título de la tesis: Bases de gÁ¶bner: desarrollo formal en coq
- Autor: Gilberto Pérez Vega
- Universidad: A coruña
- Fecha de lectura de la tesis: 21/01/2005
Dirección y tribunal
- Director de la tesis
- Barja Pérez José Mª
- Tribunal
- Presidente del tribunal: Freire nistal José Luis
- Manuel Ojeda aciego (vocal)
- inmaculada Perez de guzman molina (vocal)
- felipe Gago couso (vocal)
