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

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.

A description is given for the use of a proof checker for

propositional calculus. An example of its use as well as the M and

S expressions for the proof checker are also included.

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.