**Deductive Synthesis Of The Unification Algorithm**

by Manna, Zohar and Waldinger, Richard

Technical Note 246

Institution: AI Center, SRI International

Address: 333 Ravenswood Ave., Menlo Park, CA 94025

Jul 1981.

The deductive approach is a formal program construction method in which the derivation of a program from a given specification is regarded as a theorem-proving task. To construct a program whose output satisfies the conditions of the specification, we prove a theorem stating the existence of such an output. The proof is restricted to be sufficiently constructive so that a program computing the desired output can be extracted directly from the proof. The program we obtain is applicative and may consist of several mutually recursive procedures. The proof constitutes a demonstration of the correctness of this program. To exhibit the full power of the deductive approach, we apply it to a nontrivial example–the synthesis of a unification algorithm. Unification is the process of finding a common instance of two expressions. Algorithms to perform unification have been central to many theorem-proving systems and to some programming-language processors. The task of deriving a unification algorithm automatically is beyond the power of existing program synthesis systems. In this paper we use the deductive approach to derive an algorithm from a simple, high-level specification of the unification task. We will identify some of the capabilities required of a theorem-proving system to perform this derivation automatically.

Adobe PDF |
BibTeX |
EndNote |

Name | Title | ||
---|---|---|---|

Waldinger, Richard J | Principal Scientist |

©2015 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493

SRI International is an independent, nonprofit corporation. Privacy policy

SRI International is an independent, nonprofit corporation. Privacy policy