A. YONEZAWA and C. HEWITT 41 REPRESENTATIONS FOR ABSTRACT REASONING 4 A maximal method for set variables in automatic theorem-proving W. W. BLEDSOE

References are to text of chapters, not to the bodies of bibliographies.

A new predicate calculus deduction system based on production rules is proposed. The system combines several developments in Artificial Intelligence and Automatic Theorem Proving research including the use of domain-specific inference rules and separate mechanisms for forward and backward reasoning. It has a clean separation between the data base, the production rules, and the control system. Goals and subgoals are maintained in an AND/OR tree structure. We introduce here a structure that is the dual of the AND/OR tree to represent assertions. The production rules modify these structures until they "connect" in a fashion that proves the goal theorem. Unlike some previous systems that used production rules, ours is not limited to rules in Horn Clause form. Unlike previous PLANNER-like systems, ours can handle the full range of predicate calculus expressions including those with quantified variables, disjunctions, and negations.

The two favoured theoretical bases for languages have been lambda calculus as advocated by Landin and others, and predicate calculus as advocated by Kowalski (see Landin (1966) and Kowalski (1973)). In this paper I adopt an approach based on predicate calculus, but in a manner that differs from the existing PROLOG language (Warren 1975 and Battani & Meloni 1973) in that I adopt a "forward inference" approach -- inferring conclusions from premises, rather than the "backward inference" approach of PROLOG, which starts with a desired conclusion and tries to find ways of inferring it. This difference is reflected in the internal structure of the associated implementations, that of PROLOG being a "backtrack search" kind of implementation, while the most obvious implementation of the system proposed here involves a kind of mass operation on tables of data, reminiscent of APL (Iverson 1962) but in fact identical in many respects with the work of Codd (Codd 1970) on relational data bases. Indeed, from one perspective this paper can be seen as an extension of Codd's work into the realm of general purpose computing. As in the case of PROLOG it is necessary for the user of the relational programming system to make statements which are not associated with the logical structure of the problem, but reflect the need to control the computation. In PROLOG these are effected by the use of extra-logical control primitives, but in our system control is exercised by the introduction of predicates for that purpose, which have exactly the same semantics as the predicates relevant to the logical structure of the problem. In later sections I deal with the problem of introducing equality into the system, in a way that reflects the normal mathematical usage of equality.

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