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.