back icon
close icon

Capture phrases in quotes for more specific queries (e.g. "rocket ship" or "Fred Lynn")

Journal Article  August 1, 1992

Fundamentals Of Deductive Program Synthesis

SRI Authors Richard J. Waldinger


An informal tutorial is presented for program synthesis, with an emphasis on deductive methods. According to this approach, to construct a program meeting a given specification, we prove the existence of an object meeting the specified conditions. The proof is restricted to be sufficiently constructive, in the sense that, in establishing the existence of the desired output, the proof is forced to indicated a computational method for finding it. That method becomes the basis for a program that can be extracted from the proof. The exposition is based on the deductive-tableau system, a theorem-proving framework particularly suitable for program synthesis. The system includes a nonclausal resolution rule, facilities for reasoning about equality, an a well-founded induction rule.

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you. Expect a response within 48 hours.

Our Privacy Policy