A program that checks proofs in J. A. Robinson's formulation of

predicate calculus has been programmed in LISP 1.5. The program is

available in CTSS at Project MAC and is also available as a card

deck. The program is used for class exercises at Stanford.

This paper is a discussion of several methods for the connection of

a television camera to the PDP-1 computer. Three of these methds

are discussed in detail and have in common that only a 36 bit

portion of any horizontal scanning line may be read and this

information is read directly into the working registers of the

computer. The fourth involves a data channel to read information

directly into the core memory of the computer, and is mentioned only

in passing. The major concepts and some of the details of these

methods are due to Marvin Minsky.

The following is an excerpt from a proposal to ARPA and gives some

of the project plans for the near future.

The purpose of this paper is to identify and discuss a number of

theoretical problems whose solutions seem feasible and likely to

advance the practical art of computation. The problems that will be

discussed include the following:

1. Semantics of programming languages. What do the strings of

symbols representing computer programs, statements, declarations,

labels, etc., denote? How can the semantics of programming

languages be described formally?

2. Data spaces. What are the spaces of data on which computer

programs act and how are they built up up from simpler spaces?

3. How can time dependent and simultaneous processes be described?

4. Speed of computation. What can be said about how much

computation is required to carry out certain processes?

5. Storage of information. How can information be stored so that

items identical or similar to a given item can be retrieved?

6. Syntax directed computation. What is the appropriate domain for

computations described by productions or other data format

recognizers?

7. What are the appropriate formalisms for writing

proofs that computer programs are equivalent?

8. In the view of Godel's theorem that tells us that any formal

theory of computation must be incomplete, what is a reasonable

formal system that will enable us to prove that programs terminate

in practical cases?

SIMPLE SIMON is a program which solves the problem of finding an

object satisfying a predicate from a list of facts. It operates by

backward chaining. The rules of procedure and heuristics are

discussed and the structure of the program is outlined.

A discussion of the programming and hardware characteristics of the

analog to digital converter on the PDP-1 is given; several sample

programs are also presented.

Using the formalism of the Newell-Shaw-Simon General Problem Solver

to solve problems expressed in McCarthy's Advice Taker formalism is

discussed. Some revisions of the formalism of and

described in AI Memo 2 are proposed.

A description of the programming required to utilize the TV camera

connected to the PDP-1 and of the initial collection of programs.

An example of a typical Advice-Taker axiomatization of a situation is given, and the situation is programmed in LISP as an indication

of how the Advice-Taker could be expected to react. The situation

chosen is the play of a hand of bridge.

An exposition of the MacMahon Squares problem together with some 'theoretical' results on the nature of its solutions and a short discussion of an ALGOL program which finds all solutions are

contained herein.

Program execution time can be reduced, by a considerable amount, by optimizing the 'For-loops' of Algol programs. By judicious use of index registers and by evaluating all the sub-expressions whose

values are not altered within the 'For-loop', such optimization can be achieved.

In this project we develop an algorithm to optimize Algol programs in list-structure form and generate a new source language program, which contains the 'desired contents in the index registers' as a

part of the For-clause of the For-statement and additional statements for evaluating the same expressions outside the 'For-loop' This optimization is performed only for the innermost 'For-loops'.

The program is written entirely in LISP. Arrays may have any number of subscripts. Further array declarations may have variable dimensions. (Dynamic allocation of storage.) The program does not

try to optimize arithmetic expressions. (This has already been extensively investigated.)