# Accession Number:

## ADA107328

# Title:

## Deductive Synthesis of the Unification Algorithm,

# Descriptive Note:

# Corporate Author:

## STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

# Personal Author(s):

# Report Date:

## 1981-06-01

# Pagination or Media Count:

## 52.0

# Abstract:

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 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. Author

# Descriptors:

# Subject Categories:

- Theoretical Mathematics
- Computer Programming and Software