author = {B. Buchberger},
title = {{Algorithmic Algorithm Synthesis: Case Study Gröbner Bases}},
language = {english},
abstract = {We present a new method, called "lazy thinking", for the algorithmic synthesis of algorithms from formal specifications. The method proceeds by trying out various algorithm schemes for the given problem. An algorithm scheme is a recursive function definition whose subalgorithms are unspecified. For each scheme, an (automated) proof of the correctness of the scheme w.r.t. the given problem specification is attempted. Such an attempt will normally fail because nothing is known about the subalgorithms. However, from the failing proof attempt, by a "specification generation algorithm", we can often generate specifications for the subalgorithms that will make the correctness proof work. Now we can apply the lazy thinking method recursively to the subalgorithms until we arrive at specifications that are met by algorithms in the available algorithm library. The method has been implemented in the Theorema system and is successful in numerous examples of problem specification, e.g. in the area of sorting. In the talk we will show how the method can be applied to synthesize automatically the main idea of current Groebner bases algorithms, namely the notion of S-polynomials.},
year = {2005},
month = {March 12},
annote = {2005-03-12-A},
note = {Invited talk at University of Ohio, Ashland, USA},
conferencename = {University of Ohio, Ashland, USA}