We present an algorithm that takes a first-order sentence φ in full arithmetic with arrays (with quantification over numbers, and with numerical terms serving as array indices), and builds a test formula that can be used to determine which indices of φ's constituent arrays “really” occur. We call this concept syntactic dependence. We show how to use syntactic dependence as a test for semantic dependence, i.e., the true dependence of φ on the value of an array element. This is useful in truth-maintenance systems or symbolic execution systems, where a sentence may be true in one state but false in the next. More specifically, if we are given an initial state, a sentence (such as φ above) that is true in the initial state, and a list of array elements that may be changing value during a state transition, the algorithm can be used to determine whether φ must remain true after the state transition.

No abstract available.

Liveness and safety properties are discussed from the standpoints of their topological characterizations and their expressibility in a state transition language with added invariants. The strengths of the languages obtained by varying the exact definition of the interval of invariance are analyzed. With the help of the topological characterizations, it is shown that pure liveness cannot be used to prove safety.>

The construction of term-rewriting systems, specifically by the Knuth–Bendix completion procedure, is considered. We look for conditions that might ensure the existence of a finite canonical rewriting system for a given equational theory and that might guarantee that the completion procedure will find it. We define several notions of equivalence between rewriting systems in the ordinary and modulo case, and examine uniqueness of systems and the need for backtracking in implementing completion.

The relation M1 ⊰ M2, where M1 and M2 are elementary submodels of a given model M, defines a partial ordering ⊰(M). A natural question is: What are the general properties of this ordering and what special properties can it have for given M? Here we give an example of a prime model M for which ⊰(M) is a dense linear order, in particular ⊰(M) is isomorphic to the natural order of (− ∞, ∞], the reals with a last element (Theorem 1). In fact, this is the only way for ⊰(M) to be a linear order when M is prime (Theorem 3). We then remark that if N is a model of an ℵ0-categorical theory then ⊰(N) cannot be a linear order, but we give an example where ⊰(N) is a dense partial order, N a model of an ℵ0-categorical theory. Independently, and about the same time, Benda [1] found nonprime models M where ⊰(M) is isomorphic to any one of a large class of orders, including (− ∞, ∞]. His methods are very similar to ours. Notation. We assume the reader is familar with Vaught [2] where he will find the definitions and standard results pertaining to prime models, homogeneous models, and ℵ0-categorical theories.