Since production systems were first proposed in 1943 as a general

computational mechanism, the methodology has seen a great deal of

development and has been applied to a diverse collection of problems.

Despite the wide scope of goals and perspectives demonstrated by the

various systems, there appear to be many recurrent themes. This

paper is an attempt to provide an analysis and overview of those

themes, as well as a conceptual framework by which many of the

seemingly disparate efforts can be viewed, both in relation to each

other, and to other methodologies.

Accordingly, we use the term 'production system' in a broad sense,

and attempt to show how most systems which have used the term can be

fit into the framework. The comparison to other methodologies is

intended to provide a view of PS characteristics in a broader

context, with primary reference to procedurally-based techniques, but

with reference also to some of the current developments in

programming and the organization of data and knowledge bases.

This is a slightly revised version of a paper to appear in %2Machine

Representations of Knowledge%*, Dordrecht, D. Reidel Publishing

Company (1976).

"Obviously true" properties of programs can be hard to prove when meanings are

specified with a denotational semantics. One cause of this is that such a

semantics usually abstracts away from the running process - thus properties

which are obvious when one thinks about this lose the basis of their

obviousness in the absence of it. To enable process-based intuitions to

be used in constructing proofs one can associate with the semantics an

abstract interpreter so that reasoning about the semantic can be done by

reasoning about computations on the interpreter. This technique is used

to prove several facts about a semantics of pure LISP. First a denotational

semantics and an abstract interpreter are described. Then it is shown that

the denotation of any LISP form is correctly computed by the interpreter. This

is used to justify an inference rule - called "LISP-induction" which

formalises induction on the size of computations on the interpreter. Finally

LISP-induction is used to prove a number of results. In particular it is

shown that the function eval is correct relative to the semantics - i.e.

that it denotes a mapping which maps forms (coded asd S-expressions) on to

their correct values.

The MYCIN system has begun to exhibit a high level of performance as a

consultant on the difficult task of selecting antibiotic therapy for

bacteremia. This report discusses issues of representation and design for

the system. We describe the basic task and document the constraints

involved in the use of a program as a consultant. The control structure and

knowledge representation of the system are examined in this light, and

special attention is given to the impact of production rules as a

representation. The extent of the domain independence of the methodology

is also examined.

The paper investigates methods for applying an on-line interactive

verification system designed to prove properties of PASCAL programs.

The methodology is intended to provide techniques for developing a

debugged and verified version starting from a program, that - is

possibly unfinished in some respects, - may not satisfy the required

specifications,i.e., may contain bugs, - may be incompletely

documented in the sense that the assertions provided by the

programmer are not sufficient for proving correctness. It deals with

programs that may be written in non-standard ways, e.g., permits user

defined data structures.

The methodology involves - techniques for describing data structures,

type constraints, and properties of programs and subprograms (i.e.

lower level procedures); - the use of (abstract) data types in

structuring programs and proofs. - interactive application of a

verification condition generator, an algebraic simplifier and a

theorem-prover;

Within each unit (i.e. segment of a problem), the interactive use is

aimed at reducing verification conditions to manageable proportions

so that the non-trivial factors may be analysed. Analysis of

verification conditions attempts to localize errors in the program

logic, to extend assertions inside the program, to spotlight

additional assumptions on program subfunctions beyond those already

specified by the programmer, and to generate appropriate lemmas and

assumptions that allow a verification to be completed. Methods for

structuring correctness proofs are discussed.

A detailed case study of a pattern matching algorithm illustrating

the various aspects of the methodology (including the role played by

the user) is given.

This is a reference manual for FAIL, a fast, one-pass assembler for

PDP-10 and PDP-6 machine language. FAIL statements,

pseudo-operations, macros, and conditional assembly features are

described. Although FAIL uses substantially more main memory than

MACRO-10, it assembles typical programs about five times faster.

FAIL assembles the entire Stanford time-sharing operating system (two

million characters) in less than four minutes of CPU time on a KA-10

processor. FAIL permits an ALGOL-style block structure which

provides a way of localizing the usage of some symbols to certain

parts of the program, such that the same symbol name can be used to

mean different things in different blocks.

Man-machine dialogues using everyday conversational English present

difficult problems for computer processing of natural language.

Grammar-based parsers which perform a word-by-word, parts-of-speech

analysis are too fragile to operate satisfactorily in real time

interviews allowing unrestricted English. In constructing a

simulation of paranoid thought processes, we designed an algorithm

capable of handling the linguistic expressions used by interviewers

in teletyped diagnostic psychiatric interviews. The algorithm uses

pattern-matching rules which attempt to characterize the input

expressions by progressively transforming them into patterns which

match, completely or fuzzily, abstract stored patterns. The power of

this approach lies in its ability to ignore recognized and

unrecognized words and still grasp the meaning of the message. The

methods utilized are general and could serve any "host" system which

takes natural language input.