ALGORITHM INVENTION AND VERIFICATION BY LAZY THINKING
Bruno Buchberger · 2004
In this paper, we study algorithm invention and verification as a specific variant of systematic theory exploration and propose the "lazy thinking paradigm" for inventing and verifying algorithms automatically; i.e., for a given predicate logic specification of the problem in terms of a set of operations (functions and predicates), the method produces an algorithm that solves the problem together with a correctness proof for the algorithm. In the ideal case, the only information that has to be provided by the user consists of the formal problem specification and a complete knowledge base for the operations that occur in the problem specification. The "lazy thinking paradigm" is characterized .