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 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. The algorithm scheme is a definition 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 specifications for the unknown subalgorithms. Algorithms that satisfy the generated specifications 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. },
year = {2008},
translation = {0},
school = {Research Institute for Symbolic Computation (RISC)},
length = {157}