@**phdthesis**{RISC3425,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.
},

year = {2008},

translation = {0},

school = {Research Institute for Symbolic Computation (RISC)},

length = {157}

}