Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory

This thesis is concerned with the implementation of the “lazy thinking” synthesis method in the frame of the mathematical assistant system Theorema and its application to the synthesis of algorithms in the theory of Gröbner bases. The “lazy thinking” method, proposed by Bruno Buchberger, the first advisor of this thesis, is part of his model of systematic theory exploration based on knowledge schemes. Essentially, lazy thinking is a deductive, scheme-based synthesis method: a proof of the correctness of an algorithm (i.e. its specification) using an algorithm scheme and using complete knowledge about the specification is attempted. All definitions and properties of concepts involved in the specifications are known.