We describe Microalgol, a trivial subset of Algol, by means of an interpreter. The notions of abstract syntax and of 'state of the computation' permit a compact description of both syntax and semantics. We advocate an extension of this technique as a general

way of describing programming language.

A formal model for representing control in production systems is defined.

The formalism allows control to be directly specified independently of the

conflict resolution scheme, and thus allows the issues of control and

nondeterminism to be treated separately. Unlike previous approaches, it

allows control to be examined within a uniform and consistent framework.

It is shown that the formalism provides a basis for implementing control

constructs which, unlike existing schemes, retain all the properties

desired of a knowledge based system --- modularity, flexibility,

extensibility and explanatory capacity. Most importantly, it is shown

that these properties are not a function of the lack of control

constrains, but of the type of information allowed to establish these

constraints.

Within the formalism it is also possible to provide a meaningful notion of

the power of control constructs. This enables the types of control

required in production systems to be examined and the capacity of various

schemes to meet these requirements to be determined.

Schemes for improving system efficiency and resolving nondeterminism are

examined, and devices for representing such meta-level knowledge are

described. In particular, the objectification of control information is

shown to provide a better paradigm for problem solving and for talking

about problem solving. It is also shown that the notion of control

provides a basis for a theory of transformation of production systems, and

that this provides a uniform and consistent approach to problems involving

subgoal protection.

Organic Chemical Synthesis is found to be a suitable program for developing

machine intelligence. A previous paper described the objective and global

characteristics of the project. The present article aims to describe the

program organization as a heuristic search, the design of the Problem Solving

Tree and the search procedures in considerable detail. Examples of syntheses

discovered and the problem solving tree developed are given. The programs

are written mostly in PL1(F) applicable to an IBM 360/67 and the timings

(batch mode) indicate that we have fast and efficient practical systems.

Adam Coates for acrobatic flight maneuvers of the Stanford autonomous helicopter. Autonomous helicopter flight is widely regarded to be a highly challenging control problem. It is particularly difficult to design controllers for non-stationary maneuvers in which the helicopter goes through various flight regimes, extensively exposing the great complexity of helicopter dynamics. Despite these challenges, human experts can reliably fly helicopters through a wide range of maneuvers, including aerobatic maneuvers at the edge of the helicopter's capabilities.

Pieter Abbeel and Adam Coates developed apprenticeship learning algorithms that leverage expert demonstrations to efficiently learn good controllers for the tasks being demonstrated by an expert. These apprenticeship learning algorithms have enabled their helicopters to significantly extend the state of the art in autonomous helicopter flight and aerobatics. Their experimental results included the first autonomous execution of a wide range of maneuvers, including flips, rolls, loops, auto-rotation landings, chaos and tictocs, which only exceptional human pilots can perform. Their results also included complete air shows, which required autonomous transitions between many of these maneuvers. Their system performs as well, and often even better, than an expert human pilot.

The formal structure of aesthetics systems is defined. Aesthetics systems

provide for the essential tasks of interpretation and evaluation in

aesthetic analyis. Kolmogorov's formulation of information theory is

applicable. An aesthetics system for a class of non-representational,

geometric paintings and its application to three actual paintings is

described in the Appendix.

The objectives of the research reported here are to develop an

automated decision process for real time allocation of defense

missiles to attacking ballistic missiles in general war and to

demonstrate the effectiveness of applying heuristic learning to seek

optimality in the process. The approach is to model and simulate a

missile defense environment and generate a decision procedure

featuring a self-modifying, heuristic decision function which

improves its performance with experience. The goal of the decision

process that chooses between the feasible allocations is to minimize

the total effect of the attack, measured in cumulative loss of

target value. The goal is pursued indirectly by considering the

more general problem of maintaining a strong defense posture, the

ability of the defense system to protect the targets from both

current and future loss.

The objectives of the research reported here are to develop an

automated decision process for real time allocation of defense

missiles to attacking ballistic missiles in general war and to

demonstrate the effectiveness of applying heuristic learning to seek

optimality in the process. The approach is to model and simulate a

missile defense environment and generate a decision procedure

featuring a self-modifying, heuristic decision function which

improves its performance with experience. The goal of the decision

process that chooses between the feasible allocations is to minimize

the total effect of the attack, measured in cumulative loss of

target value. The goal is pursued indirectly by considering the

more general problem of maintaining a strong defense posture, the

ability of the defense system to protect the targets from both

current and future loss.

A program which performs 'obvious' (non-controversial) simplifying

transformations on algebraic expressions (written in LISP prefix

notation) is described. Cancellation of inverses and consolidation

of sums and products are the basic accomplishments of the program;

however, if the user desires to do so, he may request the program to

perform special tasks, such as collect common factors from the

products in sums or expand products. Polynomials are handled by

routines which take advantage of the special form by polynomials; in

particular, division (not cancellation) is always done in terms of

polynomials. The program (run on the IBM 7090) is slightly faster

than a human; however, the computer does not need to check its work

by repeating the simplification.

Although the program is usable -- no bugs are known to exist -- it

is by no means a finished project. A rewriting of the simplify

system is anticipated; this will eliminate much of the existing

redundancy and other inefficiency, as well as implement an

identity-recognizing scheme.

We describe an on-line program for algebraic simplification. The

program is written in LISP 1.5 for the Q-32 computer at System

Development Corporation in Santa Monica, California. The program

has in its entirety been written and debugged from a teletype

station at Stanford University.

This paper describes KRL, a Knowledge Representation Language designed for

use in understander systems. It outlines both the general concepts which

underlie our research and the details of KRL-0, an experimental

implementation of some of these concepts. KRL is an attempt to integrate

procedural knowledge with a broad base of declarative forms. These forms

provide a variety of ways to express the logical structure of the

knowledge, in order to give flexibility in associating procedures (for

memory and reasoning) with specific pieces of knowledge, and to control

the relative accessibility of different facts and descriptions. The

formalism for declarative knowledge is based on %2structured conceptual

objects%* with associated %2descriptions%*. These objects form a network

of %2memory units%* with several different sorts of linkages, each having

well-specified implications for the retrieval process. Procedures can be

associated directly with the internal structure of a conceptual object.

This %2procedural attachment%* allows the steps for a particular operation

to be determined by characteristics of the specific entities involved.

The control structure of KRL is based on the belief that the next

generation of intelligent programs will integrate data-directed and

goal-directed processing by using multi-processing. It provides for a

priority-ordered multi-process agenda with explicit (user-provided)

strategies for scheduling and resource allocation. It provides

%2procedure directories%* which operate along with %2process frameworks%*

to allow procedural parameterization of the fundamental system processes

for building, comparing, and retrieving memory structures. Future

development of KRL will include integrating procedure definition with the

descriptive formalism.

An information processing model of some important aspects of

inductive reasoning is presented within the context of one

scientific discipline. Given a collection of experimental (mass

spectrometry) data from several chemical molecules the computer

program described here separates the molecules into "well-behaved"

subclasses and selects from the space of all explanatory processes

the "characteristic" processes for each subclass. The definitions of

"well-behaved" and "characteristic" embody several heuristics which

are discussed. Some results of the program are discussed which have

been useful to chemists and which lend credibility to this approach.

A systematic method of identification of all possible graph isomers

consistent with a given empirical formula is described. The method,

embodied in a computer program, generates a complete list of isomers.

Duplicate structures are avoided prospectively.

Methods for verifying programs written in a higher level programming

language are devised and implemented. The system can verify programs

written in a subset of PASCAL, which may have data structures and

control structures such as WHILE, REPEAT, FOR, PROCEDURE, FUNCTION

and COROUTINE. The process of creation of verification conditions is

an extension of the work done by Igarashi, London and Luckham which

is based on the deductive theory by Hoare. Verification conditions

are proved using specialized simplification and proof techniques,

which consist of an arithmetic simplifier, equality replacement

rules, fast algorithm for simplifying formulas using propositional

truth value evaluation, and a depth first proof search process. The

basis of deduction mechanism used in this prover is Gentzen-type

formal system. Several sorting programs including Floyd's TREESORT3

and Hoare's FIND are verified. It is shown that the resulting array

is not only well-ordered but also a permutation of the input array.

We present here an axiomatic approach which enables one to prove by

formal methods that his program is "totally correct" (i.e., it

terminates and is logically correct -- does what it is supposed to

do). The approach is similar to Hoare's approach for proving that

a program is "partially correct" (i.e., that whenever it terminates

it produces correct results). Our extension to Hoare's method lies in

the possibility of proving correctness and termination at once, and

in the enlarged scope of properties that can be proved by it.

The Logic for Computable Functions (LCF) is being promoted as a

superior formal language for discussion of the problems of

Mathematical Theory of Computation (MTC). To this end, several

examples of MTC problems have been formalized and proofs have been

exhibited using the LCF proof-checker. However, in these examples

there has been a certain amount of ad-hoc-ery in the proofs in

that maay mathematical theorems have been assumed without proof and

no axiomatisation of the mathematical domains involved was given.

This paper describes a suitable mathematical environment for future

LCF experiments and its axiomatic basis. The environment developed

deemed appropriate for such experiments, consists of a large body of

theorems from the areas of integer arithmetic, list manipulation and

finite set theory.

Landing a 5000 pound package on Mars that would spend a year looking for life and making other measurements has been proposed. We believe that this machine should be a stored program computer with sense and motor organs and that the machine should be mobile. We discuss the following points:

1. Advantages of a computer controlled system.

2. What the computer should be like.

3. What we can feasible do given the present state of work on artificial intelligence.

4. A plan for carrying out research in computer controlled experiments that will make the Mars machine as effective as possible.

This memo gives empirical justification for the assumption that the

number of bisections of an NxN (N even) checkerboard is

approximately given by the binomial coefficient (A, A/2) where 2A is

the length of the average bisecting cut.

A compiling algorithm is given which maps a class of Algol-like

programs into a class of machine language programs. The semantics,

i. e., the effect of execution, of each class is specified, and

recursion induction used to prove that program semantics is

preserved under the mapping defined by the compiling algorithm.

This is a preprint of a paper given at the Symposium of Mathematical

Aspects of Computer Science of the American Mathematical Society

held April 7 and 8, 1966. It contains a proof of the correctness

of a compiler for arithmetic expressions.

A computer program has been written which can generate all the

structural isomers of a chemical composition. The generated

structures are inspected for forbidden substructures in order to

eliminate structures which are chemically impossible from the

output. In addition, the program contains heuristics for

determining the most plausible structures, for utilizing

supplementary data, and for interrogating the on-line user as to

desired options and procedures. The program incorporates a memory

so that past experiences are utilized in later work.