Algorithm Synthesis by Lazy Thinking: Examples and Implementation in Theorema
Bruno Buchberger, Adrian Crăciun · Electronic Notes in Theoretical Computer Science · 2004
Recently, we proposed a systematic method for top-down synthesis and verification of lemmata and algorithms called “lazy thinking method” as a part of systematic mathematical theory exploration (mathematical knowledge management). The lazy thinking method is characterized: by using a library of theorem and algorithm schemes and by using the information contained in failing attempts to prove the schematic theorem or the correctness theorem for the algorithm scheme for inventing lemmata or requirements for subalgorithms, respectively.