K.A.PATON 411 24 Centromere finding: some shape descriptors for small chromosome outlines.

The solution to this simple problem would then guide the solution of the original problem. Minsky (1961) has discussed complex planning of this'homomorphic model' type, and has stressed the potential reduction in total search effort to be won. In the same paper he has also considered the use of semantic models' as a form of complex planning in a mathematical context. The successful geometry theorem-proving program of Gelernter (1959), which used a diagram' to test the validity of propositions, is a wellknown example of this form of planning. Recently Sandewall (1969) has defined a Planning Problem Solver (P P This is an attempt to explore in detail complex planning of the homomorphic model' type as applied to the

A formal description is given of GT 4, a revised and extended version of the Graph Traverser. Methods are described whereby GT4 can improve its performance at run time (a) by automatic optimization of parameters used by the evaluation function and (b) by dynamic re-ordering of operators. Neither method depends upon there being any successful searches in the program's past experience of a given problem. The essential feasibility of both approaches has been validated in experimental tests using sliding block puzzles. Two planned extensions, 'local smoothing' and'regionalization' are described. INTRODUCTION The Graph Traverser (Doran and Michie 1966), and subsequent work based on it, represents an attempt to adapt game-playing methods, particularly those of Samuel (1959), to automatic problem-solving. The design objective is not the simulation of human problem-solving as a study in psychology, but rather to provide an efficient general-purpose search procedure appropriate to non-numerical problem domains. There is a parallel with the development of direct search techniques for numerical function minimization, for example pattern search (Hooke and Jeeves 1961), simplex (Spendley, Hext and Himsworth 1962, Nelder and Mead 1965).

In particular its task domain is the analysis of mass spectra, chemical data gathered routinely from a relatively new analytical instrument, the mass spectrometer. This collaboration of chemists and computer scientists has produced what appears to be an interesting program from the viewpoint of artificial intelligence and a useful tool from the viewpoint of chemistry. For this discussion it is sufficient to say that a mass spectrometer is an instrument into which is put a minute sample of some chemical compound and out of which comes data usually represented as a bar graph. This is what is referred to here as the mass spectrum. The x-points of the bar graph represent the masses of ions produced and the y-points represent the relative abundances of ions of these masses. The first, preliminary inference (or planning), obtains clues from the data as to which classes of chemical compounds are suggested or forbidden by the data.

We will define the notions of abstract theorem-proving graph, abstract theorem-proving problem g and search strategy E for g. These concepts generalize the usual tree (or graph) searching problem and admit Hart, Nilsson and Raphael (1968) and Pohl (1969) theories of heuristic search. In particular the admissibility and optimality theorems of Hart, Nilsson and Raphael generalize for the classes 0 and 0" of diagonal search strategies for abstract theorem-proving problems. In addition the subclass au of 0 is shown to be optimal for 2. Implementation of diagonal search is treated in some detail for theorem-proving by resolution rules (Robinson 1965). SEARCH STRATEGIES, COMPLETENESS AND EFFICIENCY Completeness and efficiency of proof procedures can be studied only in the context of search strategies. A system T of inference rules and axioms can be complete or incomplete for a given class of intended interpretations. Similarly a search strategy E for T may or may not be complete for ...

The equivalence problem for program schemes, or for programs, is reduced to the proving of a theorem in second-order logic. This work extends Manna's first-order logic reductions. Some examples of the technique are given together with a suggested method for obtaining proofs in special cases by firstorder methods. INTRODUCTION Several workers in recent years have considered using techniques and ideas of various mathematical theories of computation for proving interesting results about computer programs. This paper is concerned with two of these approaches.

R.M.BURSTALL 373 23 Assertions: programs written without specifying unnecessary order.

Networks as models of word storage: G. R. Kiss

SEARCH TREES We will talk about problems with the following characteristics: (i) We could recognise a solution to the problem if given one. Let us call the set of objects which is known to contain the solutions the'candidates'. We include cases where there is more than one solution or where an optimal solution is required. Some examples are: (i) In playing chess there are only a finite number of possible strategies (candidates) but the number is far too large to enumerate. Any assignment is a candidate and there are a finite, but usually large, number of assignments. The candidates are the (n -- I)! permutations of the points omitting the starting point. In this section we will describe in an abstract way two approaches to problems of this type. We will give examples of their use, first in'Some problems about sets' (p. Although both the approaches have often been used before, the discussion may help to clarify those features common to the different applications. Our two approaches are both search techniques (partial enumeration techniques).

MRS stands for Meta-level Representation System. If your response to this is a knowing nod of understanding you can probably skip the first few chapters. In a sense, MRS is a computer language, in that one enters text in a designated syntax and it gets processed and produces answers (or not). But because MRS is also able to reason with the information you give it, the'program' you enter can be seen more as representing facts than specifying a process. The importance and utility of this difference will become clear.