Personal tools
You are here: Home / Projects / DK1: Formal Theory and Algorithmics of Noncommutative Gröbner Bases

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

Supervisor: Prof. Bruno Buchberger

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