INTUITION

Author: Pérez Vega Gilberto.
Year: 2004.
University: A CORUÑA [www.udc.es].
Place of defense: Facultad de Informática.
Place of preparation: Facultad de Informática.

Summary: First, addresses, so adjusted to what was going to take, the more practical notions Coq system that are necessary to understand the formalization of the mathematical theory of polynomials, and their reduction bases Grà ¶ bner. The specific work begins with the formalization of the terms of n variables, as well as the more usual operations polynomials in the system Coq. It implements the order lexicográfico deepened proof that the order was well founded. To formalize the ring of polynomials in several variables, described evidence of the structure of body abstract. It implement polynomials and canonical polynomials, formalizing an equality explicit polynomials original description of its operations. It implements the order polynomials proving to be noetheriano.Asimismo, it implements the concept of ideal. It generalizes, in the system of Coq, the algorithm of the division of polynomials in several variables. Once implemented this division, called reduction; explores the relationship between consistency and reduction, obtaining the normal form a set of polynomials. Finally, it introduces the concept of base Grà ¶ bner, studying and testing their equivalence with other characterizations alternatives. To resolve these equivalencies is a version of the motto of Newman, implementing a scheme recursion on canonical polynomials, as well as properties of the confluence of the reduction.