INTUITION

Autor: Pérez Vega Gilberto.
Jahr: 2004.
Universität: A CORUÑA [www.udc.es].
Ort der Lesung: Facultad de Informática.
Ort der Vorbereitung: Facultad de Informática.

Inhaltsangabe: Erstens, Adressen, so angepasst, was zu nehmen, die mehr praktische Begriffe Coq System, die notwendig sind, um die Formalisierung der mathematischen Theorie der Polynome und ihre Reduzierung Grundlagen Grà ¶ bner. Die spezifische Arbeit beginnt mit der Formalisierung der Begriffe von n Variablen, sowie die üblichen Operationen Polynome im System Coq. Es implementiert die Reihenfolge lexicográfico vertieft Beweis dafür, dass sich die Reihenfolge war begründet. Zur Formalisierung der Ring der Polynome in mehreren Variablen, beschrieben Beweis für die Struktur der Körper abstrakt. Es umzusetzen Polynome und kanonischen Polynome, Formalisierung der Gleichstellung explizit Polynome ursprünglichen Beschreibung der Vorgänge. Es implementiert die Reihenfolge Polynome erweist sich als noetheriano.Asimismo führt sie das Konzept der ideal ist. Er verallgemeinert, in der das System der Coq, den Algorithmus der Division von Polynomen in mehreren Variablen. Sobald dieser Sparte umgesetzt werden, die Reduzierung; erkundet das Verhältnis zwischen Kohärenz und Reduktion, um die normale Form einer Reihe von Polynomen. Schließlich, so führt das Konzept der Basis Grà ¶ bner, Studium und Prüfung ihrer Gleichwertigkeit mit anderen Charakterisierungen Alternativen. Um diese Äquivalenzen ist eine Version des Motto Newman, der Umsetzung eines Systems Rekursion auf kanonische Polynome, sowie Eigenschaften der Zusammenfluss der Ermäßigung.