Catalogue of Artificial Intelligence Techniques
Deductive Program Synthesis
Aliases: Extracting Answers from Proofs
Keywords: Program synthesis
Categories: Automatic Programming
Author(s): Richard Waldinger
Program synthesis is the derivation of a program to meet a given specification. According to the deductive approach, program synthesis is regarded as a theorem-proving task. The system proves the existence of an output that satisfies the specification. This proof is restricted to be constructive in the sense that it must indicate a computational method of finding the output. This method becomes the basis for a program that is extracted from the proof.
- Manna Z. and Waldinger R., The Logical Basis for Computer Programming
, vol. 1, Addison-Wesley, Reading, Mass. and London, 1985.