Adrian Crăciun
West University of Timişoara, Timişoara, Romania

Lazy Thinking is a deductive, scheme-based synthesis method, proposed by Bruno Buchberger as part of a mathematical theory exploration model and implemented to some extent in the Theorema system. Lazy Thinking works as follows: try to prove the correctness of an algorithm (i.e. its specification) using an algorithm scheme (algorithmic idea). All definitions and properties of concepts involved in the specifications are known. The proof is likely to fail, since the proposed algorithmic solution has "holes", i.e. is expressed in terms of unknown components. 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 components. 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 give some examples of scheme-based theory exploration, including the synthesis of a Groebner Bases algorithm.