**Subproblem finder and instance checker, two cooperating modules for theorem provers**

Dennis de Champeaux

Pages: 633-657

DOI: 10.1145/6490.6491

Properties are proved about INSTANCE, a theorem prover module that recognizes that a formula is a special case and/or an alphabetic variant of another formula, and about INSURER, another theorem prover module that decomposes a problem,...

**The combinatorics of local constraints in model-based recognition and localization from sparse data**

W. Eric L. Grimson

Pages: 658-686

DOI: 10.1145/6490.6492

The problem of recognizing what objects are where in the workspace of a robot can be cast as one of searching for a consistent matching between sensory data elements and equivalent model elements. In principle,...

**On driving many long wires in a VLSI layout**

Vijaya Ramachandran

Pages: 687-701

DOI: 10.1145/6490.6784

It is assumed that long wires represent large capacitive loads, and the effect on the area of a VLSI layout when drivers are introduced along many long wires in the layout is investigated. A layout is presented for which the introduction of...

**Approximating grammar probabilities**: solution of a conjecture

R. Chaudhuri, A. N. V. Rao

Pages: 702-705

DOI: 10.1145/6490.214099

It is proved that the production probabilities of a probabilistic context-free grammar may be obtained as the limit of the estimates inferred from an increasing sequence of randomly drawn samples from the language generated by the grammar....

**Initializing generalized feedback shift register pseudorandom number generators**

Bruce Jay Collings, G. Barry Hembree

Pages: 706-711

DOI: 10.1145/6490.6493

The generalized feedback shift register pseudorandom number generators proposed by Lewis and Payne provide a very attractive method of random number generation. Unfortunately, the published initialization procedure can be extremely time...

**Complexity of parallel QR factorization**

M. Cosnard, Y. Robert

Pages: 712-723

DOI: 10.1145/6490.214102

An optimal algorithm to perform the parallel QR decomposition of a dense matrix of size N is proposed. It is deduced that the complexity of such a decomposition is asymptotically 2N, when an unlimited number of...

**Countable nondeterminism and random assignment**

K. R. Apt, G. D. Plotkin

Pages: 724-767

DOI: 10.1145/6490.6494

Four semantics for a small programming language involving unbounded (but countable) nondeterminism are provided. These comprise an operational semantics, two state transformation semantics based on the Egli-Milner and Smyth orders, respectively,...

**RECAL—a new efficient algorithm for the exact analysis of multiple-chain closed queuing networks**

A. E. Conway, N. D. Georganas

Pages: 768-791

DOI: 10.1145/6490.6495

RECAL, a Recursion by Chain Algorithm for computing the mean performance measures of product-form multiple-chain closed queuing networks, is presented. It is based on a new recursive expression...

**How to construct random functions**

Oded Goldreich, Shafi Goldwasser, Silvio Micali

Pages: 792-807

DOI: 10.1145/6490.6503

A constructive theory of randomness for functions, based on computational complexity, is developed, and a pseudorandom function generator is presented. This generator is a deterministic polynomial-time algorithm that transforms pairs...

**Polynomial-time algorithm for the orbit problem**

R. Kannan, R. J. Lipton

Pages: 808-821

DOI: 10.1145/6490.6496

The accessibility problem for linear sequential machines [12] is the problem of deciding whether there is an input *x* such that on *x* the machine starting in a given state *q*_{1} goes to a given state...