Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleGroebner bases - Theory Refinement in the Mizar System
Author(s) Christoph Schwarzweller
TypeArticle in Conference Proceedings
AbstractWe argue that for building mathematical knowledge repositories a broad development of theories is of major importance. Organizing mathematical knowledge in theories is an obvious approach to cope with the immense number of topics, definitions, theorems, and proofs in a general repository that is not restricted to a special field. However, concrete mathematical objects are often reinterpreted as special instances of a general theory, in this way reusing and refining existing developments. We believe that in order to become widely accepted mathematical knowledge management systems have to adopt this flexibility and to provide collections of well-developed theories.
As an example we describe the Mizar development of the theory of Groebner bases, a theory which is built upon the theory of polynomials, ring (ideal) theory, and the theory of rewriting systems. Here, polynomials are considered both as ring elements and elements of rewriting systems. Both theories (and polynomials) already have been formalized in Mizar and are therefore refined and reused. Our work also includes a number of theorems that, to our knowledge, have been proved mechanically for the first time.
CopyrightSpringer Verlag
SeriesLecture Notes in Artificial Intelligence
PublisherSpringer Verlag
Translation No
Refereed No
Conferencename4th International Conference on Mathematical Knowledge Management