INTUITION

Auteur: Pérez Vega Gilberto.
Année: 2004.
Université: A CORUÑA [www.udc.es].
Lieu de l'exposition: Facultad de Informática.
Lieu de préparation: Facultad de Informática.

Résumé: Premièrement, les adresses, ainsi ajusté à ce qui se passait à prendre, la plus pratique les notions Coq système qui sont nécessaires pour comprendre la formalisation de la théorie mathématique des polynômes, et de leurs bases de réduction Grà ¶ bner. Le travail commence par la formalisation des termes de n variables ainsi que de la plus fréquente des polynômes opérations dans le système Coq. Il met en oeuvre l'ordre lexicográfico approfondir la preuve que l'ordre était bien fondée. Pour formaliser l'anneau de polynômes en plusieurs variables, a décrit la preuve de la structure du corps abstrait. Il appliquer polynômes et canonique des polynômes, officialisant une égalité explicite polynômes description original de ses opérations. Il met en oeuvre l'ordre polynômes révèle être noetheriano.Asimismo, il met en oeuvre le concept de l'idéal. Elle généralise, dans le système de Coq, l'algorithme de la division des polynômes à plusieurs variables. Une fois mis en œuvre cette division, appelée réduction; explore la relation entre la cohérence et la réduction, l'obtention de la forme normale d'un ensemble de polynômes. Enfin, il introduit le concept de base de Grà ¶ bner, d'étudier et de tester leur équivalence avec d'autres caractérisations d'alternatives. Pour résoudre ces équivalences est une version de la devise de Newman, l'application d'un schéma de récursion sur les polynômes canoniques, ainsi que les propriétés de la confluence de la réduction.