Details:
Title  Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory  Author(s)  Adrian Craciun  Type  Technical Report, Misc  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, schemebased 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 criticalpair completion algorithm scheme, we show how our implementation can be applied successfully to ef fectively (re)invent the idea of Spolynomials (as outlined by Bruno Buchberger), and complete a proof of correctness.  Length  157 
URL 
http://www.risc.jku.at/publications/download/risc_3424/thesisAC.pdf 
Language  English  Number  0802  Year  2008  Month  April  Translation 
No  Refereed 
No 
