The Heurisic DENDRAL program uses an information processing model of

scientific reasoning to explain experimental data in organic

chemistry. This report summarizes the organization and results of the

program for computer scientists. The program is divided into three

main parts: planning, structure generation, and evaluation.

The planning phase infers constraints on the search space from the

empirical data input to the system. The structure generation phase

searches a tree whose termini are models of chemical models using

pruning heuristics of various kinds. The evaluation phase tests the

candidate structures against the original data. Results of the

program's analyses of some tests are discussed.

We discuss the class of program schemas augmented with equality

tests, that is, tests of equality between terms. In the first part

of the paper we illustrate the "power" of equality tests. It turns

out that the class of program schemas with equality is more powerful

than the "maximal" classes of schemas suggested by other

investigators. In the second part of the paper, we discuss the

decision problems of program schemas with equality. It is shown, for

example, that while the decision problems normally considered for

schemas (such as halting, divergence, equivalence, isomorphism and

freedom) are decidable for ianov schemas. They all become

undecidable if general equality tests are added. We suggest,

however, limited equality tests which can be added to certain

subclasses of program schemas while preserving their decidability

property.

Heuristic DENDRAL is a computer program written to solve problems of

inductive inference in organic chemistry. This paper will use the

design of Heuristic DENDRAL and its performance on different problems

for a discussion of the following topics:

l. the design for generality;

2. the performance problems attendent upon too

much generality

3. the coupling of expertise to the general problem solving

processes,

4. the symbiotic relationship between generality and

expertnness of problem solving systems.

We conclude the paper with a view of the design for a general problem

solver that is a variant of the "big switch" theory of generality.

An elementary outline of the theorem-proving approach to automatic

program synthesis is given, without dwelling on technical details.

The method is illustrated by the automatic construction of both

recursive and iterative programs operating on natural numbers, lists,

and trees.

In order to construct a program satisfying certain specifications, a

theorem induced by those specifications is proved, and the desired

program is extracted from the proof. The same technique is applied

to transform recursively defined functions into iterative programs,

frequently with a major gain in efficiency.

It is emphasized that in order to construct a program with loops or

with recursion, the principle of mathematical induction must be

applied. The relation between the version of the induction rule used

and the form of the program constructed is explored in some detail.