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 noncommutative Gröbner bases in a completely formal  (logic) frame, namely the Theorema version of predicate logic. In the first part of the thesis, using and extending the Theorema automated formal reasoning tools, 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. The  subtle relation of (noncommutative) Gröbner bases theory with linear algebra based on the notion of generalized Sylvester matrix, which has significant potential for improving the algorithmics but was never carefully and completely studied theoretically, should be investigated in detail using the formal theory and the formal exploration tools provided in the first part of the thesis. If possible in the frame of just one thesis, one major application of noncommutative Gröbner bases theory, e.g. cryptography, should be explored and implemented. The thesis will also serve as an important input into  a major research project "Math Journals as Active Reasoning Agents" by the same proposer in cooperation with a renowned international mathematics publishing company and will be carried out in close cooperation with the currently most active research groups in noncommutative Gröbner bases theory worldwide.

Supervisor: Prof. Bruno Buchberger