**Theorem Proving with Lemmas**

G. E. Peterson

Pages: 573-581

DOI: 10.1145/321978.321979

The concern here is with proof procedures which are generalizations of input or unit deduction. The author's generalizations of input deduction involve lemmas, whereas those of unit deduction involve longer clauses and are akin to Robinson's P1...

**Size complexity in context-free grammars forms**

Seymour Ginsburg, Nancy Lynch

Pages: 582-598

DOI: 10.1145/321978.321980

Grammar forms are compared for their efficiency in representing languages, as measured by the sizes (i.e. total number of symbols, number of variable occurrences, number of productions, and number of distinct variables) of interpretation...

**Boundary and Object Detection in Real World Images**

Yoram Yakimovsky

Pages: 599-618

DOI: 10.1145/321978.321981

A computer solution to the problem of automatic location of objects in digital pictures is presented. A self-scaling local edge detector that can be applied in parallel on a picture is described. Clustering algorithms and sequential boundary...

**Mathematical Techniques for Efficient Record Segmentation in Large Shared Databases**

Mark J. Eisner, Dennis G. Severance

Pages: 619-635

DOI: 10.1145/321978.321982

It is possible to significantly reduce the average cost of information retrieval from a large shared database by partitioning data items stored within each record into a primary and a secondary record segment. An analytic model, based upon...

**Accelerated Iterative Methods for the Solution of Tridiagonal Systems on Parallel Computers**

D. E. Heller, D. K. Stevenson, J. F. Traub

Pages: 636-654

DOI: 10.1145/321978.321983

Iterative methods for the solution of tridiagonal systems are considered, and a new iteration is presented, whose rate of convergence is comparable to that of the optimal two-cyclic Chebyshev iteration but which does not require the calculation...

**Sequencing Jobs with Stochastic Task Structures on a Single Machine**

John L. Bruno

Pages: 655-664

DOI: 10.1145/321978.321984

A sequencing problem wherein there is a single processor and a finite number of jobs needing service is considered. Each job consists of a sequence of tasks generated probabilistically by a finite state Markov chain. Each state in the Markov...

**Open Shop Scheduling to Minimize Finish Time**

Teofilo Gonzalez, Sartaj Sahni

Pages: 665-679

DOI: 10.1145/321978.321985

A linear time algorithm to obtain a minimum finish time schedule for the two-processor open shop together with a polynomial time algorithm to obtain a minimum finish time preemptive schedule for open shops with more than two processors are...

**Multilevel Queues with Extremal Priorities**

Z. Rosberg, I. Adiri

Pages: 680-690

DOI: 10.1145/321978.321986

This paper deals with a single server serving N priority classes (N being finite or infinite) and working under an FBz regime, namely, one in which the waiting line consists of infinitely...

**Verifying Program Performance**

Ben Wegbreit

Pages: 691-699

DOI: 10.1145/321978.321987

It is shown that specifications of program performance can be formally verified. Formal verification techniques, in particular, the method of inductive assertions, can be adapted to show that a program's maximum or mean execution time is...

**Enumeration of Fanout-Free Boolean Functions**

John P. Hayes

Pages: 700-709

DOI: 10.1145/321978.321988

A solution to the problem of counting the number of fanout-free Boolean functions of n variables is presented. The relevant properties of fanout-free functions and circuits are summarized. The AND and OR ranks of a fanout-free...

**A Combinatorial Problem Which Is Complete in Polynomial Space**

S. Even, R. E. Tarjan

Pages: 710-719

DOI: 10.1145/321978.321989

This paper considers a generalization, called the Shannon switching game on vertices, of a familiar board game called Hex. It is shown that determining who wins such a game if each player plays perfectly is very hard; in fact, if this game...

**Space and Time Hierarchies for Classes of Control Structures and Data Structures**

R. J. Lipton, S. C. Eisenstat, R. A. DeMillo

Pages: 720-732

DOI: 10.1145/321978.321990

Control structures and data structures are modeled by directed graphs. In the control case nodes represent executable statements and arcs represent possible flow of control; in the data case nodes represent memory locations and arcs represent...

**The Semantics of Predicate Logic as a Programming Language**

M. H. Van Emden, R. A. Kowalski

Pages: 733-742

DOI: 10.1145/321978.321991

Sentences in first-order predicate logic can be usefully interpreted as programs. In this paper the operational and fixpoint semantics of predicate logic programs are defined, and the connections with the proof theory and model theory of logic...