연사 : Bruno Buchberger교수(Johannes Kepler University)
제목 : "Algorithmic Algorithm Synthesis: Case Study Groebner Bases"
일시 : 2004. 10.29(금), 16:00
장소 : 수학과 세미나실 2411호
초록 : Recently, we introduced a new method, called "Lazy Thinking", for the algorithmic invention of algorithms. The method starts from a given formal specifications of a problem in predicate logic and tries out various algorithm schemes from a library of possible algorithm schemes.
An algorithm scheme is a recursive definition of an algorithm in terms of unspecified auxiliary functions. For each algorithm scheme in the library, the method tries an (automated) correctness proof w.r.t. to the given problem specification. Normally, this proof will fail because nothing is known about the unspecificied subalgorithms. From the failing proof, the method automatically generates specifications for the unknown subalgorithms that will guarantee that the correctness proof can be completed. Now, there are two possibilities: Either we know algorithms that meet the specifications generated for the subalgorithms. Then we are done, i.e. we have synthesized an algorithm for the original problem. Or we apply the lazy thinking method recursively to the specifications of the unknown subalgorithms until we arrive at problem specifications that can be met by known algorithms.
We implemented the method in our Theorema system, which is a software system for mathematical theory exploration. Recently, we were able to show that the method is powerful enough to synthesize the author's Groebner bases algorithm, which is deemed to be a nontrivial algorithm in the area of computer algebra and, hence, may well serve as a benchmark for the logical power of algorithm synthesis methods.
In the talk, we will explain the method and, in particular, the synthesis of the Groebner bases algorithm in detail. We will finally draw some conclusions for the methodology of algorithmic mathematics, for the future of mathematical software systems, and for the future education of mathematics and computer science students.