Planning and Imperative Program Synthesis: A Deductive Approach
Abstract
A theorem proving framework is developed particularly well suited to the program synthesis application. In this framework, a deductive tableau of assertions and goals is manipulated, with declarative sentences each associated with a term, called its output entry. While the assertions and goals of the tableau are all that we need for a pure theorem-proving task, the output entries are required for extracting a program from a proof. The deduction rules of the framework introduce new assertions and goals with associated output entries, without changing the meaning of the tableau. These rules incorporate some of the most prominent theorem-proving techniques, including (non-clausal) resolution, mathematical induction, and term rewriting.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 26, 1990
- Accession Number
- ADA220533
Entities
People
- Richard Waldinger
Organizations
- SRI International