author = {Adrian Craciun},}

title = {{Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory}},

language = {english},

abstract = {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 ﬁrst 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 speciﬁcation) using an algorithm scheme and using complete knowledge about the speciﬁcation is attempted. All deﬁnitions and properties of concepts involved in the speciﬁcations are known. The algorithm scheme is a deﬁnition of the desired algorithm in terms of unknown subalgorithms. The proof is likely to fail, as no information about the unknown subalgorithms is available. Following an analysis of the failing proof, conjectures are generated and added to the knowledge, such that the failure can be overcome. These conjectures turn out to be speciﬁcations for the unknown subalgorithms. Algorithms that satisfy the generated speciﬁcations can then either be retrieved from the knowledge base, or synthesized by lazy thinking in subsequent rounds of exploration. We describe the method of lazy thinking and then describe its implementation in Theo- rema: • the cascade mechanism, that implements the lazy exploration cycles (initiate proof, proof failure analysis, conjecture generation), • failure analysis, and • conjecture generation. We then describe the usage of the cascade mechanism in conjunction with the reasoners available in the system. The problem of Gröbner bases represents a nontrivial benchmark for program synthesis. We present how, following an outline proposed by Bruno Buchberger, the lazy thinking implementation can be used in this case study. Starting from a critical-pair completion algorithm scheme, we show how our implementation can be applied successfully to ef- fectively (re)invent the idea of S-polynomials (as outlined by Bruno Buchberger), and complete a proof of correctness. },

number = {08-02},

year = {2008},

month = {April},

length = {157},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}