Commutative Algebra in the Mizar System
| Autor: | Andrzej Trybulec, Christoph Schwarzweller, Piotr Rudnicki |
|---|---|
| Rok vydání: | 2001 |
| Předmět: |
Power series
Algebra and Number Theory Formal power series Generalization Algebraic structure 0102 computer and information sciences 02 engineering and technology Mizar system Hilbert's basis theorem Computer Science::Digital Libraries 01 natural sciences Algebra Computational Mathematics symbols.namesake Development (topology) 010201 computation theory & mathematics Computer Science::Mathematical Software 0202 electrical engineering electronic engineering information engineering symbols Calculus 020201 artificial intelligence & image processing Commutative algebra Mathematics |
| Zdroj: | Journal of Symbolic Computation. 32:143-169 |
| ISSN: | 0747-7171 |
| DOI: | 10.1006/jsco.2001.0456 |
| Popis: | We report on the development of algebra in the Mizar system. This includes the construction of formal multivariate power series and polynomials as well as the definition of ideals up to a proof of the Hilbert basis theorem. We present how the algebraic structures are handled and how we inherited the past developments from the Mizar Mathematical Library (MML). The MML evolves and past contributions are revised and generalized. Our work on formal power series caused a number of such revisions. It seems that revising past developments with an intent to generalize them is a necessity when building a database of formalized mathematics. This poses a question: how much generalization is best? |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect