Algorithm Synthesis by Lazy Thinking: Examples and Implementation in Theorema
| Autor: | Bruno Buchberger, Adrian Crăciun |
|---|---|
| Rok vydání: | 2004 |
| Předmět: |
Scheme (programming language)
Correctness Theoretical computer science General Computer Science Computer science Theorema computer.software_genre algorithm verification program synthesis Theoretical Computer Science requirement engineering learning from failure algorithm schemes conjecture generation computer.programming_language biology Programming language merging Frame (networking) lazy thinking mathematical knowledge retrieval re-usable algorithms biology.organism_classification Mathematical knowledge management merge-sort Mathematical theory algorithm invention algorithm correctness didactics of programming mathematical knowledge management computer Algorithm sorting Computer Science(all) |
| Zdroj: | Electronic Notes in Theoretical Computer Science. 93:24-59 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2003.12.027 |
| Popis: | 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. In this paper, we give a couple of examples for algorithm synthesis using the lazy thinking paradigm. These examples illustrate how the synthesized algorithm depends on the algorithm scheme used. Also, we give details about the implementation of the lazy thinking algorithm synthesis method in the frame of the Theorema system. In this implementation, the synthesis of the example algorithms can be carried out completely automatically, i.e. without any user interaction. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect