Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

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.



Add Comment

No comments.