# DK1: Formal Theory and Algorithmics of Noncommutative Gröbner Bases

The goal of this thesis is a thorough
presentation of the theory and algorithmics
of (non)commutative Gröbner bases in a
completely formal (logic) frame, namely the
Theorema version of predicate logic.
In the first part of the thesis, the subtle
relation of Gröbner bases theory with linear
algebra based on the notion of generalized
Sylvester matrix should be investigated and the potential
of this relation for improving the
algorithmics of Gröbner bases construction should be studied.

Using and extending the Theorema automated formal
reasoning tools, if possible, the theory should
be formally verified and, using the Theorema
functor programming paradigm, the algorithmics
should be implemented in a generic, and also formally verified, way.

Supervisor: Prof. Bruno Buchberger