Christoph Schwarzweller
We prove the correctness of the generic algorithms of Brown and Henrici concerning addition and
multiplication in fraction fields of gcd domains. For that we
first prove some basic facts about divisibility in integral domains and introduce the concept of
amplesets. After that we are able to define gcd domains and to
prove the theorems of Brown and Henrici which are crucial for the correctness of the algorithms.
In the last section we define Mizar functions mirroring the algorithms'
input/output behaviour and prove properties of these functions that ensure the correctness of
the algorithms.
Christoph Schwarzweller
Although generic programming finds more and more attention---nowadays generic
programming languages as well as generic libraries exist---there are hardly approaches for
the verification of generic algorithms or generic libraries. This thesis deals with generic
algorithms in the field of computer algebra.
We propose the Mizar system as a theorem prover capable of verifying generic algorithms
on an appropriate abstract level. The main advantage of the Mizar theorem prover is its special input
language that enables textbook style presentation of proofs. For generic versions
of Brown/Henrici addition and of Euclidan's algorithm we give complete correctness
proofs written in the Mizar language.
Moreover, we do not only prove algorithms correct in the usual sense. In addition we show
how to check, using the Mizar system, that a generic algebraic algorithm is
correctly instantiated with a particular domain. Answering this question that especially
arises if one wants to implement generic programming languages, in the field of
computer algebra requires non trival mathematical knowledge.
To build a verification system using the Mizar theorem prover, we also implemented
a generator which almost automatically computes for a given algorithm a set of theorems that imply
the correctness of this algorithm.
Christoph Schwarzweller
We introduce the field of quotients over an integral domain following the well-known
construction using pairs over integral domains. In addition we define ring
homomorphisms and prove some facts about these fields including their universal property.
Christoph Schwarzweller
In this paper we give Mizar formalization of concept lattices. Concept lattices stem
from so-called formal concept analysis - a part of applied mathematics that
brings mathematical methods into the field of data analysis and knowledge processing.
Our approach follows the one given in Wille, Ganter; Formale Begriffsanalyse.
Christoph Schwarzweller
In this article we introduce the ring of Integers, Euclidean rings and Integers modulo p.
In particular we prove that the Ring of Integers is an Euclidean ring
and that the Integers modulo p constitute a field if and only if p is a prime.
Rüdiger Loos, David R. Musser, Sibylle Schupp, Christoph Schwarzweller
Tecton is an algebraic specification language. This report contains a considerable
body of Tecton concepts which evolved over a long time. The concepts serve as a test
bed for a Tecton translator and are a formal basis for declarations occurring in
algorithms from all areas of programming but in particular from comouter algebra.
Christoph Schwarzweller
In this article we define noetherian and co-noetherian lattices and show how some
properties concerning upper and lower neighbours, irreducibility and density can
be improved when restricted to these kinds of lattices. In addition we define atomic
lattices.
Christoph Schwarzweller
In this article we continue the formalization of concept lattices following "Wille, Ganter;
Formale Begriffsanalyse". We prove a theorem stating necessary and sufficient conditions for
a complete lattice to be isomorphic to a given formal context. As a by-product we get that
a lattice is complete if and only if it is isomorphic to a concept lattice. In addition we
introduce dual formal concepts and dual concept lattices.
Christoph Schwarzweller
We propose the Mizar system as a theorem prover capable of verifying generic algebraic algorithms
on an appropriate abstract level. The main advantage of the Mizar theorem prover is its special
proof script language that enables textbook style presentation of proofs, hence allowing proofs
in the language of algebra.
Using Mizar we were able to give a rigorous machine assisted correctness proof of a generic version
of the Brown/Henrici arithmetic in the field of fractions over arbitrary gcd domains.
Christoph Schwarzweller, Andrzej Trybulec
In this article we define the evaluation of multivariate polynomials and show that this
mapping constitutes a homomorphism from the ring of polynomials into the coefficient ring
(even for an infinite number of indeterminates).
Christoph Schwarzweller
In this paper we report on the Mizar codification of formal concepts and concept
lattices being part of the theory of formal concept analysis, a mathematical theory
that formally describes the notion of concepts and concept hierarchies.
We give a short introduction to the theory of concept lattices and describe how we
modelled these structures in the Mizar language. After that we discuss experiences
and problems concerning the formalization; in particular we deal with reusing
mathematical knowledge of the Mizar Mathematical Library.
Piotr Rudnicki, Christoph Schwarzweller, Andrzej Trybulec
We report on the construction of formal multivariate power series and
polynomials in the Mizar system. First, we present how the algebraic
structures are handled and how we inherited the past developments from
the Mizar library. The Mizar Mathematical library evolves and past contributions
are revised and (usually) 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 data base of formalized mathematics. And this poses a
question: how much generalization is best?
Christoph Schwarzweller
In this paper we prove the well-known binomial theorem for algebraic structures.
In doing so we tried to be as modest as possible concerning the algebraic
properties of the underlying structure. Consequently we proved the binomial
theorem for "commutative rings" in which the existence of an inverse with respect
to addition is replaced by a weaker property of cancellation.
Jonathan Backer, Piotr Rudnicki, Christoph Schwarzweller
We introduce the basic notions of ideal theory in rings. This includes left and right
ideals, (finitely) generated ideals and some operations on ideals such as the
addition of ideals and the radical of an ideal. In addition we introduce linear combinations
to formalize the well-known characterization of generated ideals.
Principal ideal domains and Noetherian rings are defined. The latter development follows
Becker, Weispfenning; Gröbner Bases, pages 144-145.
Piotr Rudnicki, Christoph Schwarzweller, Andrzej Trybulec
We report on the development of (commutative) 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 library. The Mizar library evolves and past contributions
are revised and (usually) 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 data base of formalized mathematics. This poses a
question: how much generalization is best?
Christoph Schwarzweller
The main observation of this paper is that theorems can be
considered independent of abstract domains;
they depend rather on a set of properties necessary to prove
the theorems correct.
This leads to more general theorems and hence to improved
reuse of mathematical theorems.
We discuss how this view influences the design of mathematical
libraries and illustrate our approach with examples written in
the Mizar language.
Christoph Schwarzweller
In this article we deal with some technical notion for multivariate
polynomials with arbitrary number of variables: Monomials and constant
polynomials are introduced and their properties with respect to the
eval functor are shown. In addition the multiplication of polynomials with
coefficients is defined and investigated.
Robert Milewski, Christoph Schwarzweller
The Mizar construction of polynomials with an arbitrary number of variables has already been described
and is part of the Mizar Mathematical Library.
In this paper we present an alternative approach for formalizing polynomials with one variable. This
approach has the advantage that quite a number of theorems can be proven with fewer requirements on the
underlying coefficient ring. In addition, because polynomials with only one variable can be easier
represented, the construction allows for more straightforward proofs.
Christoph Schwarzweller
We claim that mathematical databases should be more than a collection
of domains with associated theorems;
in particular theorems should be stated as general as possible, that
is independent of domains.
A database then should be able to check whether such a general theorem
holds in a particular domain.
To this end we use a properties-based representation for both theorems
and domains,
and present a deduction calculus that using additional rules about the
problem domain allows to perform such a theorem check.
Christoph Schwarzweller
In this paper we define Term Orders for an arbitrary number of variables.
Based on this headterms, headcoefficients and headmonomials as well as
the reductum of polynomials are introduced.
Basic theorems about these notions and term orders necessary to develop
the theory of Gröbner bases are proven.
Christoph Schwarzweller
In this article we continue the Mizar formalization towards Gröbner bases
following "Becker, Weispfenning; Gröbner Bases".
We introduce reduction for polynomials and prove its basic properties including
termination, adequateness for ideal congruences and the translation lemma used
later to show confluence of polynomial reduction.
Christoph Schwarzweller
Theorems can be considered independent of abstract domains;
a theorem rather depends on a set of properties necessary to prove
the theorem correct.
Following this observation theorems can be formulated and proven more generally
thereby improving reuse of mathematical theorems.
We discuss how this view influences the design of mathematical
libraries and illustrate our approach with examples written in
the Mizar language.
We also argue that this approach allows for both stating requirements
of generic algorithms and checking whether
particular instantiations of generic algorithms are semantically correct.
Christoph Schwarzweller
We continue the Mizar formalization of Gröbner bases following
"Becker, Weispfenning; Gröbner Bases".
In this article we prove a number of characterizations
of Gröbner bases among them that Göbner bases are convergent
rewriting systems. We also show the existence and uniqueness of reduced
Gröbner bases.
Christoph Schwarzweller
We continue the Mizar formalization of Gröbner bases following
"Becker, Weispfenning; Gröbner Bases".
In this article we introduce S-polynomials and standard
representations and show how these notions can be used to characterize
Gröbner bases.
back to Zakład Informatyki