Work of the Soviet school (approximately half the book) in this explosively growing area of machine intelligence is thus made accessible for the first time to Western readers, in addition to the latest Western advances. The emergent theme of knowledge-representation is supported on the theoretical and experimental sides by recent work in inductive inference and theory-formation.

PROLOG is a simple and powerful progamming language based on first-order logic. This paper examines two possible extensions to the language which would generally be considered "higher-order".t The first extension introduces lambda expressions and predicate variables so that functions and relations can be treated as'first class' data objects. We argue that this extension does not add anything to the real power of the language. The other extension concerns the introduction of set expressions to denote the set of all (provable) solutions to some goal. We argue that this extension does indeed fill a real gap in the language, but must be defined with care.

Seven years or so after it was first proposed (Kowalski 1974), the technique of'logic programming' today has an enthusiastic band of users and an increasingly impressive record of applications. For most of these people, logic progamming means PROLOG, the system defined and originally implemented by the Marseille group (Roussel 1975). PROLOG has since been implemented in several other places, most notably at Edinburgh (Warren et al. 1977). Much of the rapid success of logic progamming is due to these implementations of PROLOG (as well as to the inspired missionary work of Kowalski, van Emden, Clark and others). The Edinburgh PROLOG system is in particular a superb piece of software engineering which allows the logic progammer to compile assertions into DEC-10 machine code and thus run logic programs with an efficiency which compares favourably with that of compiled LISP. All other implementations of logic programming (including our own, which we describe in this paper) are based on interpreters.

A programming language based on sets; motivation and examples.

D.B.VIGOR 33 MECHANISED MATHEMATICS 4 An approach to analytic integration using ordered algebraic expressions. L.I.HonGsox 47 5 Some theorem-proving strategies based on the resolution principle.

K3 Th is a statement of facts and theories relevant to all the ei.

Spectra 70 / 46 and the IBM 360/50, that performs many second-order inferences in addition to carrying out first-order'resolutions' on Skolemized disjunctive formulae. The second-order aspect of the program is represented by an extended matching procedure, which operates in conjunction with rules for lambda abstraction and application, and for existential generalization and instantiation. These rules abstract properties from first-order formulae and apply axioms such as mathematical induction to these properties, thereby generating new second-order formulae as well as first-order formulae that could not have been produced by the resolution method alone. The mechanization of second-order logic is of potential usefulness in the areas of deductive question answering, illustrated by an example, and to the proving of formal properties of programs. Among the more interesting recent developments in the theory and practice of automatic theorem proving are the incorporation of formal techniques such as J. A. Robinson's resolution method into the'deductive sections' of question-answering and problem-solving systems (Chadwick et al. 1969, Green 1969), the solution of previously'open' problems (Guard et a/.

Given P {P1,.. P„} as input, set j 0, 00 8 (the identity substitution), and go to step 2. Step 2. (for j 0): if Pi0j is a singleton for each i, 1 1,.. n,

If the original formula included this function, we must also allow for its negation. This can either be eliminated or the following formula complicated to allow for this situation. However, in our examples this negation cannot appear and so we do not include it.

The distinction between analytic and empirical statements obviously has some potential philosophical overtones. We hope to avoid most of them by formulating the distinction in terms of an assumption on the verbs believe, know, and so on, rather than in terms of philosophical considerations. The predicate'Holds' The connectedness' of our set of functions and relations requires that there should be some unary relation'Holds' such that Holds(m