**Special relations in automated deduction**

Zohar Manna, Richard Waldinger

Pages: 1-59

DOI: 10.1145/4904.4905

Two deduction rules are introduced to give streamlined treatment to relations of special importance in an automated theorem-proving system. These rules, the relation replacement and relation matching rules,...

**Routing through a rectangle**

K. Mehlhorn, F. P. Preparata

Pages: 60-85

DOI: 10.1145/4904.4994

In this paper an O(N log N) algorithm for routing through a rectangle is presented. Consider an n-by-m rectangular grid and a set of N...

**An application of number theory to the organization of raster-graphics memory**

Benny Chor, Charles E. Leiserson, Ronald L. Rivest, James B. Shearer

Pages: 86-104

DOI: 10.1145/4904.4800

A high-resolution raster-graphics display is usually combined with processing power and a memory organization that facilitates basic graphics operations. For many applications, including interactive text processing, the ability to quickly move...

**Notions of dependency satisfaction**

Marc H. Graham, Alberto O. Mendelzon, Moshe Y. Vardi

Pages: 105-129

DOI: 10.1145/4904.4798

Two notions of dependency satisfaction, consistency and completeness, are introduced. Consistency is the natural generalization of weak-instance satisfaction and seems appropriate when only equality-generating...

**A chaotic asynchronous algorithm for computing the fixed point of a nonnegative matrix of unit spectral radius**

Boris Lubachevsky, Debasis Mitra

Pages: 130-150

DOI: 10.1145/4904.4801

Given a nonnegative, irreducible matrix P of spectral radius unity, there exists a positive vector &pgr; such that &pgr; = &pgr;P. If P also happens to be stochastic, then &pgr; gives the stationary distribution of the Markov chain that has...

**“Sometimes” and “not never” revisited**: on branching versus linear time temporal logic

E. Allen Emerson, Joseph Y. Halpern

Pages: 151-178

DOI: 10.1145/4904.4999

The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these...

**Bound hierarchies for multiple-class queuing networks**

Derek L. Eager, Kenneth C. Sevcik

Pages: 179-206

DOI: 10.1145/4904.4992

An algorithm for computing bounds on the performance measures of multiple-class, product-form queuing networks is presented. The algorithm offers the user a hierarchy of bounds with differing accuracy levels and computational cost requirements....

**A matrix-algebraic solution to two ***K*_{m} servers in a loop

Appie van de Liefvoort, Lester Lipsky

Pages: 207-223

DOI: 10.1145/4904.5391

An explicit steady-state solution is given for any queuing loop made up of two general servers, whose distribution functions have rational Laplace transforms. The solution is in matrix geometric form over a vector space that is itself a direct...

**Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness**

David Harel

Pages: 224-248

DOI: 10.1145/4904.4993

Elementary translations between various kinds of recursive trees are presented. It is shown that trees of either finite or countably infinite branching can be effectively put into one-one correspondence with infinitely branching trees in such a...