In this section we discuss how theorem-proving methods are being tested for several applications in the Stanford Research Institute Artificial Intelligence Group's Automaton (robot). We emphasize that this section describes work that is now in progress, rather than work that is completed. These methods represent explorations in problem solving, rather than final decisions about how the robot is to do problem solving. An overview of the current status of the entire SRI robot project is provided by Nilsson. Coles has developed an English-to-logic translator that is part of the robot.

See also: Education Resources Information CenterSupplement to Proceedings of the IFIP 68 International Congress, Edinburgh, August 1968. Published in A. J. H. Morrell (ed.), Information Processing 68, Vol. II, pp. 1008-1022, Amsterdam: North-Holland, 1969.

AN AUGMENTED STATE TRANSITION NETWORK ANALYSIS PROCEDURE Daniel G. Bobrow Bolt, Beranek and Newman, Inc. Cambridge, Massachusetts Bruce Eraser Language Research Foundation Cambridge, Massachusetts Summary A syntactic analysis procedure is described which obtains directly the deep structure information associated with an input sentence. The implementation utilizes a state transition network characterizing those linguistic facts representable in a context free form, and a number of techniques to code and derive additional linguistic information and to permit the compression of the network size, thereby allowing more efficient operation of the system. By recognizing identical constituent predictions stemming from two different analysis paths, the system determines the structure of this constituent only once. When two alternative paths through the state transition network converge to a single state at some point In the analysis, subsequent analyses are carried out only once despite the ...

Stanford AI Memo 83 or Computer Science Technical Note 130, Computer Science Department, Stanford University, Stanford, CA, 1969

Reading, Mass.: Addison-Wesley.

In IEEE Conference Record of the 1969 Tenth Annual Symposium on Switching and Automata Theory, pp. 74–81.

This term is meant to suggest not only the usual specifics of programming system and language but also such more elusive and subjective considerations as ease and level of interaction, "forgivefulness" of errors, human engineering, and system "Initiative." In normal usage, the word "environment" refers to the "aggregate of social and cultural conditions that influence the life of an individual." The programmer's enivronment influences, to a large extent determines, what sort of problems he can (and will want to) tackle, how far he can go, and how fast. If the environment is "cooperative" and "helpful" -- the anthropomorphism is deliberate -- then the programmer can be more ambitious and oroductive. If not, he will spend most of his time and energy "fighting" the system, which at times seems bent on frustrating his best efforts.

PLANNER: A LANGUAGE FOR PROVING THEOREMS IN ROBOTS Summary Carl Project MAC - Massachuse PLANNER is a language for proving theorems and manipulating models in a robot. The language is built out of a number of problem solving primitives together with a hierarchical control structure. Statements can be asserted and perhaps later withdrawn as the state of the world changes. Conclusions can be drawn from these various changes in state. Goals can be established and dismissed when they are satisfied. The deductive system of PLANNER is subordinate to the hierarchical control structure in order to make the language efficient. The use of a general purpose matching language makes the deductive system more powerful. Preface PLANNER is a language for proving theorems and manipulating models in a robot.

Many problems in artificial intelligence involve the searching of large trees of alternative possibilities--for example, game-playing and theorem-proving. The problem of efficiently searching large trees is discussed. A new method called "dynamic ordering" is described, and the older minimax and Alpha-Beta procedures are described for comparison purposes. Performance figures are given for six variations of the game of kalah. A quantity called "depth ratio" is derived which is a measure of the efficiency of a search procedure.

The problem discussed in this paper, namely that of finding a function to satisfy a given argument-value table, is by no means new to computing science, or to mathematics. Thus, for example, the problem of fitting a curve to a set of points is a part of numerical analysis. However, I am concerned with finding a function over a non-metric space, and so my work is closer to that of Feldman et al. (1969) in what they call, 'grammatical inference' or to the automaton-synthesizing programs described by Fogel, Owens and Walsh (1966).