J. Do RAN 433 22 Chromosome classification and segmentation as exercises in knowing what to expect.

The eighth volume completes a ten-year span of the Machine Intelligence series. It is appropriate, therefore, to take stock of the main events, and to note certain solid steps and occasional forward leaps. Leaps are normally preceded by some preparatory back-tracking. The uniform procedures of heuristic search and resolution theorem-proving which dominated the scene in 1965 cannot of themselves, as we now see, be developed into "the answer" to automatic problem-solving. This realisation has paved the way for machine-aided forays into non-trivial mathematics, as indicated in Bledsoe and Tyson's contribution to this volume.

Names only appear which are in no sense bibliographic references; otherwise they are to be found in the author index.]

Plan modification *The research reported herein was sponsored by the National Science Foundation under Grant GJ-36146.

To use language one must be able to make inferences about the information which language conveys. This is apparent in many ways. For one thing, many of the processes which we typically consider "linguistic" require inference making. For example, structural disambiguation: (1) Waiter, I would like spaghetti with meat sauce and wine. You would not expect to be served a bowl of spaghetti floating in meat sauce and wine. That is, you would expect the meal represented by structure (2) rather than that represented by (3).

Department of Computer Science University of Western Ontario PART 1 In their book Mathematics and Logic Kac and Ulam (1971) comment: "The point of view as it has evolved through centuries is that one need not know what things are as long as one knows what statements about them one is allowed to make. Hilbert's famous Grundlagen der Geometrie begins with the sentence: 'Let there be three kinds of objects; the objects of the first kind shall be called "points", those of the second kind "lines", and those of third "planes". That is all, except that there follows a list of initial statements (axioms) that involve the words "point', "line" and "plane", and from which other statements involving those undefined words can now be deduced by logic alone. This permits geometry to be taught to a blind man and even to a computer!" Leaving aside the attitude implicit in Kac & Ulam's use of the word'even' in the phrase even to a computer', it has become clear that programs to prove theorems in ...

B.RANDELL 3 PROGRAM PROOF AND MANIPULATION 2 Some techniques for proving correctness of programs which alter data structures.

Oberuc 245, 249 see predicate calculus Occam's razor 271 London 24-5, 52

INTRODUCTION If let loose, resolution theorem-provers can waste time in many ways. They can continually rearrange the multiplication brackets of an associative multiplication operation or replace terms t by ones like f(f(f(t, e), e), e) where f is a multiplication function and e is its identity. Generally they continually discover and misapply trivial lemmas. Global heuristics using term complexity do not help much and ad hoc devices seem suspicious. On the other hand, one would like to evaluate terms when possible, for example we would want to replace 5 4 by 9. More generally one would like to have liberty to simplify, to factorise and to rearrange terms. The obvious way to deal with an associative multiplication would be to imitate people, and just drop the multiplication brackets. However used or abused the basic facts involved in such manipulations form an equational theory, T, that is, a theory all of whose sentences are universal closures of equations. Under certain conditions, we will be able to build the equational theory into the rules of inference. The resulting method will be resolution-like, the difference being that concepts are defined using provable equality between terms rather than literal identity. Therefore the set of clauses expressing the theory will not be among the input clauses, so no time will be wasted in the misapplication of trivial lemmas, since the rules will not waste time in this way.

The frame problem in representing natural-language information is discussed. It is argued that the problem is not restricted to problem-solving-type situations, in which it has mostly been studied so far, but also has a broader significance. A new solution to the frame problem, which arose within a larger system for representing natural-language information, is described. The basic idea is to extend the predicate calculus notation with a special operator, Unless, with peculiar properties. Some difficulties with Unless are described. THE FRAME PROBLEM This paper proposes a method for handling the frame problem in representing conceptual, or natural-language-type information.