The Specialization and Transformation of Constructive Existence Proofs
Abstract
The transformation of constructive program synthesis proofs is discussed and compared with the more traditional approaches to program transformation. An example system for adapting programs to special situations by transforming constructive synthesis proofs has been reconstructed and is compared with the original implementation [Goad 80]. A brief account of more general proof transformation applications is also presented. The overall moral is that constructiveexistence proofs contain more information over and above that required for simple execution and that this can be exploited by a proof transformation system.
Cite
Text
Madden. "The Specialization and Transformation of Constructive Existence Proofs." International Joint Conference on Artificial Intelligence, 1989.Markdown
[Madden. "The Specialization and Transformation of Constructive Existence Proofs." International Joint Conference on Artificial Intelligence, 1989.](https://mlanthology.org/ijcai/1989/madden1989ijcai-specialization/)BibTeX
@inproceedings{madden1989ijcai-specialization,
title = {{The Specialization and Transformation of Constructive Existence Proofs}},
author = {Madden, Peter},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1989},
pages = {413-418},
url = {https://mlanthology.org/ijcai/1989/madden1989ijcai-specialization/}
}