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

Engeler, E., Proof theory and the accuracy of computations (to appear).

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.

COGNITIVE PROCESSES: METHODS AND MODELS 17 Steps towards a model of word selection.

INTRODUCTION The problem of reducing the line-like elements of a digitized picture to idealized thin lines is of general interest in pattern recognition. As early as 1957 the idea of obtaining a thin-line representation of certain patterns was suggested (Kirsch et al. 1957); recently McCormick (1963) and Narasimhan (1964) have described computer programs for doing this (for use in particular on bubble chamber photographs), and similar work has been done in character recognition, for example by Deutsch (1967). Blum (1964) has put forward an approach for dealing with more general shapes. In this the boundary of a shape is considered as being the source of a wavefront. The points at which wavefronts originating at different parts of the boundary first meet form a'skeleton' which, with a function giving the time taken for the wavefront to reach each point of the skeleton, completely defines the original shape. Programs for generating this skeleton for digitized pictures have been described by Rosenfeld and Pfaltz (1966), and also by Philbrick (1966).

Virginia Polytechnic Institute It is no disgrace for Scott's program to have lost to Greenblatt's which seems to be the best chess program so far written: it finished one of its games with a brilliant five-move combination.* Judging by the present game Greenblatt's program could play about board 2000 for England. Neither program seems able to form a plan that is naturally expressed-by a description rather than by evaluation functions plus analysis. In the following game the first four moves on each side were played before the machines took over the play, because the ICI, program cannot castle. The move time limits originally agreed were 90 seconds for # xEss and'blitz speed' (5 or 10 seconds per move) for the Greenblatt program, as it was considered that the P-K5, and the game has the character of a French defence difficult to evaluate.

The program contains a rough theory of mass spectrometry which is still in its formative stages.

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

The general problem of re-Presentation is concerned with the relationship between different ways of formulating a problem to a problem solving system and the efficiency with which the system can be expected to find a solution to the problem. An understanding of the relationship between problem formulation and problem solving efficiency is a prerequisite for the design of procedures that can automatically choose the most appropriate' representation of a problem (they can find a point of view' of the problem that maximally simplifies the process of finding a solution). Many problems of practical importance are problems of reasoning about actions. In these problems, a course of action has to be found that satisfies a number of specified conditions. A formal definition of this class of problems is given in the next section, in the context of a general conceptual framework for formulating these problems for computers. Everyday examples of reasoning about actions include planning an airplane trip, organizing a dinner party, etc. There are many examples of industrial and military problems in this category, such as scheduling assembly and transportation processes, designing a program for a computer, planning a military operation, etc. The research presented in this paper was sponsored in part by the Air Force Office of Scientific Research, under Contract Number A F49(638)-1184. Part of this work was done while the author was on a visiting appointment at the Computer Science Department of the Carnegie Institute of Technology, Pittsburgh, Pa.

The original intention was to demonstrate the on-line typewriter to visitors via a simple system which reacted to the user, in this case by refusing to be beaten twice in the same way at the game of Kalah. The mechanism to achieve this is a memory, built up from information obtained in previous games, which is stored on magnetic tape. The program was designed to keep the size of this memory to small proportions by implementing two mechanisms the author believes to be commonly used by humans when solving problems. The two mechanisms are: 1. ignoring irrelevant information in the sense that, although it exists, it is highly probable that its precise structure or properties cannot alter the relevant information or characteristics of the problem being considered, and 2. accepting positions close to a solution or win, providing the opponent is further from a win. Some of the difficulties of testing these ideas in practice are discussed and suggestions are made on how to overcome them, in particular with the game of solo whist.