Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems

Harald Ganzinger Max-Planck-Institut für Informatik, Saarbrücken, Germany

                              hg@mpi-sb.mpg.de

Abstract

In this paper we compare three approaches to polynomial time decidability for uniform word problems for quasivarieties. Two of the approaches, by Evans and Burris, respectively, are semantical, referring to certain embeddability and axiomatizability properties. The third approach is more proof-theoretic in nature, inspired by McAllester’s concept of local inference. We define two closely related notions of locality for equational Horn theories and show that both the criteria by Evans and Burris lie in between these two concepts. In particular, the variant we call stable locality will be shown to subsume both Evans’ and Burris’ method.

1 Introduction

This paper relates two strands of results about polynomially decidable uniform word problems for quasi-varieties. A quasi-variety is a class of algebras satisfying a particular (in this paper always finite) set K of equational Horn clauses. Given K, the uniform word problem for K is to decide whether or not an equational, variable-free Horn clause C, the query, is entailed by K: the antecedent of C are the defining relations for the generators (fresh constants) appearing there; the succedent of C is the word problem to be solved for that presentation.

One line of research leading to decidability criteria goes back to work by Skolem (Skolem 1920). Skolem considered the variety of lattices and investigated relational encodings by function-free clauses which we also call Datalog clauses today. Given a Horn theory K one can flatten the clauses such that all equations in the transformed clauses are of the form f(x_{1},... ,x_{k})≈x or x≈y with variables x_{i}, x, y. Next one can replace functions f by relations (representing their graphs) r^{f}, so that equations f(x_{1},... ,x_{k})≈x become atoms r^{f} (x_{1},... ,x_{k},x). Datalog also allows one to express that equality is an equivalence and that relations are compatible with equality. Moreover, one can specify that function graphs represent partial functions, for example, by saying r^{f} (x,y),r^{f} (x,z) → y≈z. The “only” property that is lost in the relational encoding is that functions are total. However, if one can show that all finite relational models of the encoding can be extended (maintaining K) so that the functions become total, the uniform word problem becomes (polynomially) decidable. For if the relational version C^{∗} of a flat clause C cannot be proved from the Datalog encoding K_{D} of K there will be a finite counter model for K_{D}∪ ¬C^{∗} (there are no function symbols other than the constants from C^{∗}), and if that model can be extended to one in which functions are total, this yields a model of K in which C is false. Skolem presented this technique for the special cases of lattices and for certain axiomatizations of projective geometry, but not for varieties in general. His algorithm for lattices resulting from a dynamic programming implementation of the function-free encoding was rediscovered later by Cosmadakis (1988) and by Freese (1989).^{1}

Independently of Skolem’s methods, Evans (1951) proved a somewhat stronger result for varieties in general. As Evans’ original proof is based on quite different techniques,^{2} it is not surprising that Skolem’s work is not even mentioned in his paper. Later, Burris (1995) realized that one might, in fact, view Evans’ result as a generalization of Skolem’s techniques. One of Burris’ observations was that a weak form of definedness requirements for the partial functions can also be expressed in Datalog. (For instance, one can require r^{f} (x,y) → r^{g}(x,y), expressing a relativized definedness property for the function g in terms of the definedness properties of f.) Evans’ result is that the uniform word problem is (polynomially) decidable whenever all finite partial algebras “satisfying” K can be injectively embedded into a total K-algebra, where his notion of validity for equations in partial algebras includes precisely those relativized definedness requirements expressible in Datalog (cf. Section 2 below). Having seen the connection between Skolem’s and Evans’ ideas, it was not difficult for Burris (1995) to extend Evans’ result to quasi-varieties. In the same paper he then also presented an even more general criterion for polynomial decidability that refers to the finite axiomatizability of certain classes of substructures of the relational versions of the K-algebras. We will return to this criterion in Section 7 below.

1This is how Burris (1995) puts it. Looking at the papers, however, the connections to Skolem’s work are not so obvious.

2Evans’ algorithm is ground completion — before the concept of completion was invented by Knuth & Bendix (1970) — of the antecedent of the query together with certain ground instances of the theory clauses dynamically derived from subterms of the query. Using auxiliary constants to name subterms, Evans’ procedure is closely related to recent presentations of congruence closure algorithms such as the one by Bachmair & Tiwari (2000).

The approaches of Evans and Burris emphasize the rôle of partial algebras (constructed from the subterms and the equations in the antecedent of a query) for the decidability of uniform word problems. An approach that is based on confining deduction to subterms of the query is represented by the concept of local inference systems in (Givan & McAllester 1992, McAllester 1993). Local theories are sets of Horn clauses K such that K ⊧ C, for variable-free Horn clauses C, only if already K_{C}⊧ C, where K_{C} is the set of instances of K in which all terms are subterms of ground terms in either K or C. Givan and McAllester dealt with non-equational logic whereas we are interested in the equational case. As we shall see below, the main results about non-equational local theories given in (Givan & McAllester 1992, McAllester 1993, Basin & Ganzinger 2001) can be easily extended to the equational case. In particular, the uniform word problem for local equational theories is decidable in polynomial time. A slightly more general variant of this concept is obtained by allowing in local entailment all instances K_{[C]}of K by substitutions sending the variables in K-clauses to subterms of the ground terms of C or K. We call K stably local if already K_{[C]}⊧ C whenever K ⊧ C.

The main results of this paper establish close relationships between the approaches by Evans, Burris and McAllester. We show that both Evans’ and Burris’ criteria lie in between the two variants of locality. The inclusions are (mostly) proper. In particular stable locality is shown to subsume Burris’ (and hence Evans’) method. We also show for a the subclass of superficial presentations (McAllester 1993) K that locality and embeddability coincide.

From these results we may conclude that all three criteria for polynomial decidability of uniform word problems are essentially equivalent. In the end, this might not be so surprising given that all three approaches are based on ideas of exploiting the algebraic and deductive structure, respectively, induced by the linearly many query subterms. Moreover it is known that any P-time inference problem can be encoded as a local Horn theory. However, as we shall see below, to clarify the precise relationships induces a number of technical complications mainly related to Evans’ specific notion of validity in partial algebras.

2 Basic Notions and Notation

Our investigation assumes an arbitrary, but fixed signature Σ of function symbols to be given, containing an infinite subset C of constants that are used to denote the generators in the formulation of word problems. An equational Horn clause is an implication of the form e_{1},... ,e_{k} → e_{0}, k ≥ 0, with equations e_{i} = (s_{i}≈t_{i}) over Σ. We consider the object language symbol “≈” for formal equality also syntactically as symmetric, so that s≈t at the same time also denotes t ≈s. Sometimes we also take a relational view of functions. Then, given a signature Σ, by Σ^{∗} we denote the corresponding relational signature where each n-ary function symbol f in Σ is replaced by a n + 1-ary relation symbol r^{f}. If C is an equational Horn clause with all equations of the form f(x_{1},... ,x_{k})≈x or x≈y, with variables x_{i}, x, y, by C^{∗} we denote its relational form, the Σ^{∗} clause resulting from C by replacing any equation of the form f(x_{1},... ,x_{k})≈x by an atom r^{f} (x_{1},... ,x_{k},x). (Equations between variables remain unchanged.)

Let K be a finite set of clauses, called the theory. For technical simplicity we assume that the only terms in K which are ground are constants. In equational logic this restriction can always be satisfied by flattening transformations, cf. section 4. The uniform word problem for K is to decide if K ⊧ C, for ground Horn clauses C (called queries), where “⊧” denotes implication in first-order logic with equality.

A partial (Σ)-algebra is a structure (A,{f_{A}}_{f∈Σ} ), where A is a non-empty set, and for every f ∈ Σ with arity n, f_{A} is a partial function from A^{n} to A. ^{3} Where no confusion about the interpretation of the function symbols can arise, we identify the algebra with its carrier A. For partial algebras the notion of evaluating a term t with respect to a variable assignment β for its variables, yielding a value β(t) in A, is the same as for total algebras, except that this evaluation is undefined, if t = f(t_{1},... ,t_{n}) and either one of the β(t_{i}) is undefined, or else (β(t_{1}),... ,β(t_{n})) is not in the domain of f_{A}. If the term t is ground, the evaluation is independent of any variable assignment, and its value will be denoted by t_{A}. If A ⊆ B are partial Σ-algebras, B is called an expansion of A if f_{A}= f_{B}|_{A}, the restriction of the partial function f_{B} to the subset A. A is called a (total) algebra whenever all functions are total. Under the relational view, if A is a (partial or total) Σ-algebra, by A^{∗} we denote its relational variant, the Σ^{∗}-structure for which r_{A^{∗}}^{f}(a_{1},... ,a_{n},a) is true if, and only if, f_{A}(a_{1},... ,a_{n}) = a.

Given a set K of equational Horn clauses, by K we also denote the quasi-variety represented by K, that is, the class of all total algebras that satisfy (in the usual sense of firstorder logic with equality) the clauses in K. A partial Kalgebra A is a partial algebra satisfying all the clauses in K. Hereby a clause s_{1}≈t_{1},... ,s_{k}≈t_{k} → s≈t is satisfied (is valid) in A, if for all assignments β of elements in A to the variables in the clause, whenever the β(s_{i}) and β(t_{i}) are all defined and β(s_{i}) = β(t_{i}), then

3This also includes the possibility for a constant symbol to not be defined in A.

(i) if β(s) and β(t) are both defined then β(s) = β(t); and (ii) if s = f(u_{1},... ,u_{n}), n ≥ 0, and if all terms β(u_{i}) and β(t) are defined, then β(s) is also defined.^{4} We say that a partial algebra weakly satisfies K, if only requirement (i) is satisfied for any clause in K. In a partial Kalgebra, requiring that an equation be satisfied also induces certain definedness requirements for the functions that appear in the equation. Sometimes we speak of strong satisfaction when we want to emphasize that both (i) and the definedness requirements (ii) are fulfilled.

This specific concept of validity for clauses in partial algebras was introduced by Evans. Its definedness requirements may appear ad hoc at first sight. Viewed relationally, however, one observes that this is the strongest notion of relative definedness that can directly be expressed in Datalog. For instance an equation f(g(x))≈h(x) can be encoded by writing the two clauses r^{g}(x,y),r^{f} (y,z) → r^{h}(x,z) and r^{g}(x,y),r^{h}(x,z) → r^{f} (y,z), where these two clauses imply both the equality and the definedness requirement associated with the equation. In other words, the natural encoding of conditional equations into Datalog induces the relativized definedness requirements in Evans’ definition.

As an aside, many more notions of validity have been considered in the literature, usually motivated by a particular application. One of the more prominent choices is to consider existential equality, where an equation s≈t is interpreted as “s and t are defined and are equal”. Existential equality appears to be useful for applications to the semantics of programming languages and to intuitionistic logic (Scott 1979). The treatment of partial algebras by Burmeister (1986) is also based on existential equality since most of the other notions of validity can be encoded in existential equality.

A (total) mapping h: A → B between partial Σ-algebras A and B is called a (weak) (Σ-) homomorphism if whenever f_{A}(a_{1},... ,a_{k}) is defined, then so is f_{B}(h(a_{1}),... ,h(a_{k})), and h(f_{A}(a_{1},... ,a_{k})) = f_{B}(h(a_{1}),... ,h(a_{k})). A partial Σalgebra A is said to weakly embed into K if there exists a (total) K-algebra B and an injective (weak) homomorphism from A to B.

Evans’ result (which was later extended to quasivarieties by Burris) refers to partial algebras with definedness requirements:

Theorem 2.1 (Evans 1951, Burris 1995) Let K be a finite set of Horn clauses. If every finite partial K-algebra weakly embeds into K, then the uniform word problem for K is decidable in polynomial time.

A proof of this theorem, via the relational encoding, was outlined in the introduction.

3 Local Equational Theories

Let Ψ be a set of ground terms and C a clause. By K_{Ψ} we denote the set of ground instances of K in which all terms are in Ψ. We say that K entails C with respect to Ψ, and write K ⊧_{Ψ} C, if K_{Ψ} ⊧ C.

If S is a clause or a set of clauses, by st[S] we denote the set of all ground (sub)terms appearing in S or in K. (We use this notation when K is fixed by the context. Note that we have restricted theory presentations K to only contain constants as ground terms.) A theory K is called local if for every ground Horn clause C we have K ⊧ C if, and only if, K_{st[C]}⊧ C. Whenever K_{st[C]}⊧ C we say that C is locally entailed by K. The following presentation Int of integers with successor and predecessor is local (at the end of this section we will briefly explain why):

p(x)≈y → s(y)≈x
s(x)≈y → p(y)≈x
p(x)≈p(y) → x≈y
s(x)≈s(y) → x≈y

For a local theory to decide a word problem represented by C it suffices to generate all ground instances of the theory K in which all terms are either subterms of C or constants in K and to check whether C is entailed by those ground instances. For example, the query p(s(z))≈z is entailed in equational logic by the instance s(z)≈s(z) → p(s(z))≈z of the second clause in Int.^{5} In that clause, all terms are subterms of the query. The third and fourth clauses of Int are consequences of the first two clauses. For example, s(u)≈s(v) → u≈v follows from s(u)≈s(u) → p(s(u))≈u and s(v)≈s(v) → p(s(v))≈v. However, in this derivation there appear terms (such as p(s(u))) which are not admitted in local entailment. Hence, although the injectivity clauses are entailed by the other clauses, for the presentation to be local they cannot be deleted. This is a general phenomenon. For a presentation to be local, sufficiently many consequences must be present — in particular those consequences which are not entailed by local implication. Clearly, locality is a property of a presentation rather than a property of the quasi-variety.

If the size of K is considered as a constant, the set K_{st[C]} is a finite set of equational ground clauses the size of which is polynomially bounded by C. In the non-equational case when ≈ is interpreted as an arbitrary binary relation symbol, applying the result of Dowling & Gallier (1984), we observe that entailment of queries for local theories is decidable in polynomial time. We will show that this result can be extended also to the equational case as local implication is independent of whether or not equality is internal or external.

4Remember that symmetry of ≈ is built into the notation so that the same property is also assumed to hold when exchanging s and t.

5Note that z is formally a constant here. But since it does not occur anywhere else, proving p(s(z))≈z is the same as showing Int ⊧ ∀z(p(s(z))≈z).

Let us use ⊧ and ⊧_{neq} to denote implication in logic with equality and without equality, respectively. In logic without equality, ≈ is an arbitrary binary relation symbol. Let EQ denote the set of equality axioms consisting of reflexivity, symmetry, transitivity and congruence axioms

x_{1}≈y_{1}, ... , x_{k}≈y_{k} → f(x_{1},... ,x_{k})≈f(y_{1},... ,y_{k})

for each k-ary function symbol f in the signature. In firstorder logic equality can be internalized since K ⊧ C if, and only if, K ∪ EQ ⊧_{neq} C. This carries over to local implication, the main reason being that EQ itself is a local theory (in logic without equality):

Proposition 3.1 (Givan & McAllester 1992) For any ground Horn clause C we have EQ ⊧_{neq} C if, and only if, EQ_{st[C]}⊧_{neq} C.

A consequence of this result is that congruence closure, that is, the uniform word problem for the class of all Σalgebras, is decidable in polynomial time, a result that was first proved by Kozen (1977) and later shown to be in O(nlogn) by Downey, Sethi & Tarjan (1980).

Proposition 3.2 Let S be a set of Horn clauses in which all terms are contained in a subterm-closed set Ψ of ground terms. For equalities e between terms in Ψ we have S ⊧ e if, and only if, S ∪ EQ_{Ψ} ⊧_{neq} e.

Proof. The direction from right to left is trivial. Conversely, suppose that S ⊧ e in equational logic. Then ⋃_{i}T_{S}^{i}(∅)∪ EQ ⊧_{neq} e, with T_{S} the immediate consequence operator sending interpretations I to

{e_{0} | I ∪EQ ⊧_{neq} e_{i}, for some clause e_{1},... ,e_{k} → e_{0} in S}.

From Proposition 3.1 we infer that I ∪ EQ ⊧_{neq} e_{i} only if I ∪ EQ_{Ψ_{i}} ⊧_{neq} e_{i}, where Ψ_{i} is the set of all subterms in I or in e_{i}. These terms are all in Ψ for those I obtained as T_{S}^{n}(∅), as an easy induction shows. Therefore, S ∪ EQ_{Ψ} ⊧_{neq} e. □

As an immediate consequence we obtain:

Theorem 3.3 Let S be a set of Horn clauses. Then S is a local theory in logic with equality if, and only if, S ∪ EQ is local in logic without equality.

This property of equational logic allows us to extend the results by Givan & McAllester (1992), McAllester (1993) and Basin & Ganzinger (2001) to local equational theories: Any language in P can be encoded as a uniform word problem for a local theory, that is, the method is complete for polynomial time. The set of local equational Horn theories is co-recursively enumerable but undecidable (McAllester 1993). Recursively enumerable approximations of the class of local theories as given in (McAllester 1993, Basin & Ganzinger 2001) can be easily adapted to the equational case. In particular we may use the Saturate system (Ganzinger, Nieuwenhuis & Nivela 1994) to saturate non-local presentations as described in (Basin & Ganzinger 2001). The locality of the Int example was demonstrated by Saturate by checking that all ordered resolution inferences between the clauses in Int ∪ EQ are redundant in that the respective consequences of Int ∪ EQ are entailed by smaller instances of Int ∪ EQ. This was checked for all total and well-founded extensions of the subterm ordering so that by the criterion given in (Basin & Ganzinger 2001) the locality of Int ∪ EQ follows.

Queries C for local equational theories K are decidable in polynomial time by applying dynamic programming à la Dowling & Gallier (1984) to the clauses in (S ∪ EQ)_{st[C]}. Note however that this implementation method will always give at least cubic complexity as |EQ_{st[C]}| is in Ω(n^{3}) if n is the number of terms in C. For practical applications, in particular to problems arising in program analysis (McAllester 1999), more efficient equational reasoning is required. Recent results into this direction, extending the congruence closure method of Downey et al. (1980) to conditional equations, are given in (Ganzinger & McAllester 2001).

4 Flattening and Linearity

A quasi-variety K is local if queries C are implied already by those ground instances of K in which all terms are subterms of C or K. In the equational case this property, if it is true, has to be invariant under transformations of C modulo equality. In particular, flattening transformations of C, replacing C[f(... ,t,...)] by C′ = c≉t ∨C[f(... ,c,...)], where c is a fresh constant, do not affect entailment from K, but will change the set Ψ of terms allowed in a local proof.

A ground clause is called flat if its terms have depth at most 2. A flat ground clause is called linear if whenever a constant occurs in two functional terms in the clause, the two terms are identical, and if no term contains two occurrences of a constant. Hence the clause c≈f(a,b) → f(a,b)≈f(b,a) is flat but not linear. If the clause occurs as a query, an equivalent linear query would be a≈a′,b≈b′,c≈f(a,b) → f(a,b)≈f(b′,a′), where a′ and b′ are fresh constants. For theory clauses the definition is essentially the same, with variables playing the rôle of constants: We say that a theory clause in K is flat, whenever function symbols (including constants) only occur as arguments of the equality symbol, but not as arguments of function symbols. A flat theory clause is called linear if whenever a variable occurs in two functional terms, the two terms are identical, and if no term contains two occurrences of a variable. Hence f(x,y)≈f(x,a) is neither flat nor linear. An equivalent flat and linear clause is x′ ≈x,z≈a → f(x,y)≈f(x′,z), where x′ and z are fresh variables. Clearly all clauses, queries as well as theory clauses, can be flattened (and linearized) by the introduction of auxiliary constants and variables, respectively. If K is a Horn theory, by K_{flin} we denote the set of flat and linear instances (not necessarily ground) of the clauses in K. Clearly, a non-flat clause cannot have any flat instances. A flat but non-linear clause such as a≈f(x,y) → b≈f(x′,y) has the flat and linear instance a≈f(x,y) → b≈f(x,y). Therefore, if K is finite and if subsumed clauses are ignored, K_{flin} is also finite.

Proposition 4.1 (i) If K is a local theory then K_{flin} is also local. In this case, for any query C, it holds that K ⊧ C if, and only if, K_{flin} ⊧ C. (ii) If K locally entails any flat and linear query C that is entailed by K, then K is local.

Proof. (i) Suppose that K is local. If K ⊧ C then K ⊧ flin(C), where flin(C) is the result of flattening and linearizing C. Since K is local, we obtain K_{Ψ} ⊧ flin(C), with Ψ = st[flin(C)] the set of ground subterms in flin(C) and K. As all terms in Ψ are flat and linear, and no constant occurs in more than one functional term, the clauses in K_{Ψ} are flat and linear. Therefore K_{Ψ} ⊆ (K_{flin})_{Ψ} , hence K_{Ψ} = (K_{flin})_{Ψ} . Consequently (K_{flin})_{Ψ} ⊧ C and K_{flin} is a local theory.

(ii) Suppose that K ⊧ C. We show that K_{st[C]}⊧ C. We may flatten and linearize C into C′ by using auxiliary, pairwise different constants c_{t} not occurring in K or C, to denote the subterms t of C. Specifically, we may assume that for any original subterm t = f(t_{1},... ,t_{n}) in C, C′ contains the negative equation c_{f(t_{1},...,t_{n})}≈f(c_{t_{1}},... ,c_{t_{n}}) defining the constant as an abbreviation for the respective term, and that, apart from these definitions, no other equation in C′ contains a functional term. Since K ⊧ C′, by assumption we also have K_{Ψ′} ⊧ C′, where Ψ′ is the set of ground terms in C′ or K. The only terms that may occur in K_{Ψ′} are the constants c_{t}, the constants in K, and terms of the form f(c_{t_{1}},... ,c_{t_{n}}) such that f(t_{1},... ,t_{n}) is a subterm in C. Replacing the c_{t} in K_{Ψ′} by t, therefore, yields clauses in K_{st[C]} which entail C. □

In particular, if K is local, the quasi-varieties K and K_{flin} coincide as K_{flin} also implies those instances of K which are not in K_{flin}. (The latter are trivially implied by K.) Part (ii) says that it is sufficient to show local entailment for flat, linear queries in order for a theory to be local. The relevance of this proposition is that when investigating locality for Horn theories it is sufficient to restrict attention to flat and linear theories and queries.

Flattening transformations for theory clauses that transform a clause C[f(... ,t,...)] in K into C′ = x≉t ∨ C[f(... ,x,...)], where x is a fresh variable, neither change the class of total nor the class of partial K-algebras. The same holds for linearization transformations, replacing C[f(... ,y,...)], with y a variable, by C′ = x≉y ∨ C[f(... ,x,...)], where x is a fresh variable. However replacing Γ → f(...)≈t by Γ,x≈f(...) → x≈t, although not affecting the class of total K-algebras, only preserves weak satisfaction in partial algebras. Strong satisfaction which might induce that certain f-terms be defined, are made void when this kind of transformation is performed.

5 Stably Local Theories

The proposition 4.1 also suggests that the definition of locality is sometimes too strong. In fact, the following less restrictive form of locality, where we allow arbitrary query subterms to be instantiated for the variables in theory clauses, will also be useful. Let K_{[C]}, for C a ground clause, denote the set of ground instances of clauses in K where variables are mapped to terms in st[C], that is, to subterms in C or constants in K. Considering K_{[C]}, we also have instances of K at our disposal in which there are terms not in st[C]. For example, if C = a≈b and if f(x,y)≈f(y,x) is in K then f(a,b)≈f(b,a) is in K_{[C]}but not in K_{st[C]}, since f(a,b) is not a term in C. We say that K is stably local if for every ground Horn clause C we have K ⊧ C if, and only if, K_{[C]}⊧ C. This presentation Int′ of integers with successor and predecessor is stably local even without the presence of the injectivity clauses for s and p:

p(x)≈y → s(y)≈x
s(x)≈y → p(y)≈x

In fact, s(u)≈s(v) → u≈v, say, follows from s(u)≈s(u) → p(s(u))≈u and s(v)≈s(v) → p(s(v))≈v, where these instances of Int′ are admitted in stably local entailment but not in local entailment. Rewriting the clauses of Int′ into

→ s(p(x))≈x
→ p(s(x))≈x

gives another stably local (non-flat) presentation Int′′ of the integers. For example, p(u)≈v → s(v)≈u is stably locally entailed by the instance s(p(u))≈u of the first clause in Int′′.

Locality is a special case of stable locality since K_{st[C]}= K_{[C]}_{st[C]}. Stable locality is insensitive towards flattening of goals in that for every theory K we have K_{[C]}⊧ C iff K_{[flin(C)]}⊧ flin(C). Like locality, stable locality also implies that the uniform word problem is decidable in polynomial time.

Theorem 5.1 Let K be a given theory the size of which is considered constant. If K is stably local and if C is a ground clause then K ⊧ C can be decided in time O(n^{3k}) where n is the size of C and k the maximal number of variables in any clause in K.

Proof. Let C = Γ → e. By stable locality we have K ⊧ C if, and only if, K_{[C]}∪Γ ⊧ e. From Proposition 3.2 we infer that the latter is equivalent with K_{[C]}∪Γ∪EQ_{st[K_{[C]}]∪st[C]}⊧_{neq} e. As the number of terms appearing K_{[C]}is in O(n^{k}), the size of this set of propositional Horn clauses is in O(n^{3k}). □

As Int′′ is stably local we obtain a cubic upper bound for the uniform word problem for integers with s and p.

Refined complexity bounds can be obtained by more precise analysis of the term structure in K. Although important in practice, this is not our concern here. Also, with a specialized treatment of equality one can get a better complexity bound in many cases. Using congruence closure to directly decide K_{[C]}∪Γ ⊧ e would yield a much better complexity of O(nlogn) for K = Int′′′.

6 Locality and Weak Embeddability

In this section we establish the main relationships between Evans’ embeddability criterion and locality. We will show that Evans’ criterion is weaker than stable locality but stronger than locality. For a large subclass of presentations, locality and Evans’ criterion coincide. We also show that the weaker form of Evans’ criterion with satisfaction replaced by weak satisfaction is equivalent with locality.

Looking at the proofs in (Evans 1951) it is not surprising that some sort of relation exists between embeddability and locality. However the precise details are not so straightforward, the reason being that Evan’s notion of validity, involving a semantic notion of definedness, is not so easily captured proof-theoretically. A special case is the definedness of theory constants. In this section we will additionally require that for a partial algebra A in order to satisfy, or weakly satisfy, a theory K, every constant appearing in K is defined in A. With this, Evans’ criterion becomes even stronger as fewer partial algebras need to be embedded. The restriction will only be needed for the proof of Theorem 6.1 and its applications in Section 7.

6.1 Locality Implies Embeddability

In the following theorem, under the assumption of locality, the embeddability property is even shown for infinite partial algebras that need only weakly satisfy K.

Theorem 6.1 Let K be a local set of flat Horn clauses. Then every partial algebra which weakly satisfies K weakly embeds into K.

Proof. We prove the contrapositive of the theorem. Let A be a partial algebra weakly satisfying K that does not weakly embed into K. We will show that then K is not local. Without loss of generality we may assume that A ⊆ C, that is, the elements of A are generators in Σ, but no constant occurring in K is a member of A. Moreover let Γ_{A} be the “table” of the function definitions in A, that is, the set of equations of the form f(a_{1},... ,a_{n})≈a with a, a_{j} in A and f a function symbol in Σ, such that f_{A}(a_{1},... ,a_{n}) is defined and equal to a. Suppose I is a Σ-algebra satisfying K and also the equations in Γ_{A}. The mapping h sending a in A to its value a_{I} in I is a weak Σ-homomorphism as I satisfies Γ_{A}. By assumption, A does not weakly embed into I so that there are two different elements a and a′ of A for which I ⊧ a≈a′. Hence whatever model of K ∪ Γ_{A} one chooses, it will identify two constants corresponding to different elements in A. In other words, K ∪ Γ_{A} ⊧ ⋁_{a≠a′} a≈a′. Since K ∪ Γ_{A} is a Horn theory, one of the disjuncts must be entailed, that is, K ∪ Γ_{A} ⊧ a≈a′, for two different elements a and a′ in A. Compactness of first-order logic ensures that only finitely many equations in Γ_{A}are needed to deduce a≈a′. We have shown that there is a (finite) Horn clause C = Γ → a≈a′ such that K ⊧ C, and with Γ true, but a≈a′ false in A.

Suppose that already K_{Ψ} ⊧ Γ → a≈a′, with Ψ the set of ground terms in K or C. By assumption, A weakly satisfies K. Moreover, all the terms occurring in K_{Ψ} and Γ are defined in A. Therefore, every equation in defined ground terms that is true in the least congruence generated by K_{Ψ} ∪ Γ is also true in A.^{6} But this implies that a and a′ are equal in A which is not the case. Consequently, K_{Ψ} |̸= Γ → a≈a′, hence K is not a local theory. □

Hence locality is subsumed by Evans’ criterion. This subsumption relation is proper. For the presentation Int′ one can show that every finite partial Int′-algebra weakly embeds into Int′. (In any partial Int′-algebra, s [p] must be defined on all p [s] images. Therefore both partial functions have to be injective.) However, as we have seen before, Int′ is only stably local but not local.

In the proof of the above theorem it is crucial that theory constants are defined in partial algebras that weakly satisfy K. Suppose we have K consisting of the two clauses

a≈a → a≈b
a≈b → a≈c .

Since K is equivalent to the two ground equations a≈b and a≈c, K is a local theory. But if F is a partial algebra in which a is undefined and b and c are defined but different, F vacuously satisfies K (including definedness requirements), yet cannot be weakly embedded into K.

6If a partial algebra A satisfies a set S of ground Horn clauses and if every term in S is defined in A, then if S ⊧ s≈t, with s and t defined in A, then A ⊧ s≈t. As equality is a local theory, cf. Proposition 3.1, equational reasoning can be confined to the subterms in S which are all defined in F.

6.2 Embeddability Implies Locality

Theorem 6.2 Let K be a set of flat, linear Horn clauses. Suppose that every finite partial algebra which weakly satisfies K weakly embeds into K. Then K is local.

Proof. Using the proposition 4.1, part (ii), we have to show that, under the given assumptions, if K ⊧ C, then K_{st[C]}⊧ C, for flat and linear ground clauses C. Let Ψ be shorthand notation for st[C]. As C and the clauses in K are flat, a term in Ψ is either a constant, or else of the form f(c_{1},... ,c_{n}), with constants c_{i}, n ≥ 0. Let C = s_{1}≈t_{1},... ,s_{k}≈t_{k} → s≈t, and let us assume, for the purpose of deriving a contradiction, that C is not entailed by K_{Ψ} . Then there exists an algebra I satisfying K_{Ψ} and the equations s_{i}≈t_{i}, but s and t are different in I, that is, I satisfies s≉t. From this we will now construct a finite, partial algebra F satisfying s_{i}≈t_{i} and s≉t and weakly satisfying K.

Let F = {t_{I} | t a term in Ψ}, and let the functions f in Σ be defined by f_{F}(a_{1},... ,a_{n}) = f(c_{1},... ,c_{n})_{I}, with n ≥ 0, whenever there exist constants c_{i} in Ψ such that a_{i} = c_{i}_{I}, for 1 ≤ i ≤ n, and f(c_{1},... ,c_{n}) is also a term in Ψ. Let f_{F} be undefined in all other cases. We now show that F weakly satisfies K. (By construction, F satisfies the s_{i}≈t_{i} as well as s≉t.) Clearly, the constants appearing in K are defined in F. Now let D = u_{1}≈v_{1},... ,u_{m}≈v_{m}→ u≈v be a clause in K and let β be an assignment of elements in F to the variables in D such that the β(u_{i}) = β(v_{i}), with all these terms defined. We can now find a substitution σ of the variables in D by terms in Ψ such that for every term w in D, whenever β(w) is defined then wσ is a term in Ψ and (wσ)_{I} = β(w). For instance, if a w is of the form f(x_{1},... ,x_{n}), choose x_{j}σ to be a constant c_{j} in Ψ such that c_{j}_{I} = β(x_{j}), for 1 ≤ j ≤ n, and f(c_{1},... ,c_{n}) is also a term in Ψ. (Note that the arguments to f have to be pairwise distinct variables.) By the definition of f_{F}, such constants can be found whenever f_{F} is defined on the β(x_{i}). With this, f(x_{1},... ,x_{n})σ is in fact a term in Ψ. As the entire clause D is linear in that no variable occurs in two different functional terms, the σ for the individual occurrences of functional terms can be combined into a single substitution. For variables y which do not occur in a functional term in D, the substitution can be an arbitrary term s in Ψ such that s_{I} = β(y).

We have to verify the condition (i) in the definition of satisfaction for clauses in partial algebras. Suppose that β(u) and β(v) are both defined. By the construction of σ we have that uσ and vσ are in Ψ, and (uσ)_{I} = β(u), (vσ)_{I} = β(v). With this, Dσ is in K_{Ψ} . Therefore I satisfies Dσ so that uσ_{I} = vσ_{I}, and hence β(u) = β(v). Now that F has been shown to weakly satisfy K, according to the assumption there exists a total K-algebra I′ into which F can be weakly embedded. This algebra I′ satisfies s_{i}≈t_{i}, as F does, and since the embedding is injective, I′ also satisfies s≉t. Altogether, I′ |̸= C, which contradicts the assumption that K ⊧ C. □

Hence we see that the weaker form of Evans’ criterion with satisfaction replaced by weak satisfaction implies locality. For a large subclass of presentations, the distinction between the two forms of satisfaction is inessential. Lets us call a presentation K superficial, if every term that occurs positively (in the head) of a clause in K also occurs as a subterm negatively (in the body) the same clause.

Theorem 6.3 Let K be a set of flat, linear, and superficial Horn clauses. Then K is local, whenever every finite partial K-algebra weakly embeds into K.

Proof. The definedness requirements for partial K-algebras are void, if every positive functional term also appears negatively in the same clause. In that case, any partial algebra which weakly satisfies K is a partial K-algebra, and the theorem follows from Theorem 6.2 □

For arbitrary presentations, the existence of weak embeddings for finite partial K-algebras implies stable locality.

Theorem 6.4 Let K be a set of Horn clauses. Suppose that every finite partial K-algebra weakly embeds into K. Then K is stably local.

Proof. Let C be a ground clause. We have to show that, under the given assumptions, if K ⊧ C, then K_{[C]}⊧ C. Let C = s_{1}≈t_{1},... ,s_{k}≈t_{k} → s≈t, and let us assume, for the purpose of deriving a contradiction, that C is not entailed by K_{[C]}. Then there exists an algebra I satisfying K_{[C]}and the equations s_{i}≈t_{i}, but s and t are different in I, that is, I satisfies s≉t. From this we will now construct a finite, partial K-algebra F satisfying s_{i}≈t_{i} and s≉t. The main difference to the proof of Theorem 6.2 will be that more terms are going to be defined in F.

Let F = {t_{I} | t a term in st[C]}, and let the functions f in Σ be defined such that I is an expansion of F. In other words, a function application f_{F}(a_{1},... ,a_{n}) in F is defined and yields a as result, iff f_{I}(a_{1},... ,a_{n}) = a with a in F. By construction, F satisfies the equations s_{i}≈t_{i} as well as s≉t. Let D = u_{1}≈v_{1},... ,u_{m}≈v_{m} → u≈v be a clause in K and let β be an assignment of elements in F to the variables. Then the pair D,β corresponds to at least one instance of D in K_{[C]}. And, since function application f_{F}(a_{1},... ,a_{n}) in F is defined whenever the evaluation f_{I}(a_{1},... ,a_{n}) of the application in I yields a value in F, F satisfies K such that both conditions (i) and (ii) in the definition of satisfaction are met. In other words, F is a partial K-algebra. Hence, there exists a total K-algebra I′ into which F can be embedded. This algebra I′ satisfies the equations s_{i}≈t_{i}, as F does, and since the embedding is injective, I′ also satisfies s≉t. Altogether, I′ |̸= C, which contradicts the assumption that K ⊧ C. □

The preceding theorem, in connection with Theorem 5.1, strengthens Theorem 2.1 by also providing us with a concrete complexity bound. It also shows that Evans’ approach is subsumed by stable locality. This subsumption is proper. Consider Int^{(4)} given as

p(x)≈y,s(y)≈z → z≈x
s(x)≈y,p(y)≈z → z≈x

Like Int′, the presentation Int^{(4)} is stably local. However, the two-element algebra A = {a,b} with s_{A}(a) = s_{A}(b) = a and p_{A} = ∅, the totally undefined function, trivially (strongly) satisfies Int^{(4)} but cannot be weakly embedded into Int^{(4)} where s has to be injective.

7 Locality and Axiomatizable Classes of Relational Substructures

Burris’ results are based on the view of partial algebras as relational structures. Remember that for a signature Σ without predicate symbols, by Σ^{∗} we denote the corresponding relational signature where each n-ary function symbol f in Σ is replaced by a n + 1-ary relation symbol r^{f}. Σ^{∗}-clauses are formed from the predicate symbols in Σ^{∗}, the equality symbol, and variables. Similarly, if A is a Σ-algebra, by A^{∗} we denote its relational variant, the Σ^{∗}-structure for which r_{A^{∗}}^{f}(a_{1},... ,a_{n},a) if, and only if, f_{A}(a_{1},... ,a_{n}) = a. If C is an equational Horn clause with all equations of the form f(x_{1},... ,x_{k})≈x or x≈y, with variables x_{i}, x, y, by C^{∗} we denote its relational variant where all equations f(x_{1},... ,x_{k})≈x are replaced by atoms r^{f} (x_{1},... ,x_{k},x). If K is a class of total Σ-algebras, by S(K^{∗}) we denote the class of full substructures of members of K^{∗}, that is the class of Σ^{∗}-structures A^{∗} for which there exists an algebra B in K such that B^{∗} is an expansion of A^{∗}. On the other hand, by \overline{S}(K^{∗}) we denote the class of weak substructures of members of K^{∗}. This class coincides with the class of Σ^{∗}-structures that weakly embed into K, that is, with {P^{∗} | P weakly embeds into an algebra A ∈ K}. By construction we have S(K^{∗}) ⊆ \overline{S}(K^{∗}). (A full substructure is obtained by intersecting the graphs of the functions in a total algebra with the chosen subset of its carrier. Weak substructures are obtained from full substructures by making the functions even less defined. Hence there are more weak substructures than full substructures.)

Theorem 7.1 (Burris 1995) Let K be a quasi-variety over Σ such that there is a finite set of Horn clauses H over Σ^{∗} with S(K^{∗}) ⊆ H ⊆ \overline{S}(K^{∗}). Then the uniform word problem for K is decidable in polynomial time.

The criterion says that if some subclass of relational weak substructures of K which includes all full substructures is finitely axiomatizable, the uniform word problem is decidable in polynomial time. We will show constructively that this criterion implies the existence of a stably local presentation, and that, conversely, from a local presentation a suitable H can be effectively constructed.

It is not surprising that in comparing Burris’ criterion with locality we encounter the same technical problem with constants as we did in Section 6. Hence from now on in this section we restrict the classes S(K^{∗}), H (the models of H), and \overline{S}(K^{∗}) to structures in which the relations r^{a} are nonempty, for every constant a appearing in K. In other words, if A is a partial algebra for which A^{∗} is in any of these classes, we again require that the constants in K be defined in A.

Given a set H of Σ^{∗}-clauses, by H_{∗} we denote the set of equational Σ-clauses obtained from H by replacing atoms r^{f} (x_{1},... ,x_{n},x) by equations f(x_{1},... ,x_{k})≈x. Clearly, H_{∗} is a flat set of clauses. Note that if A is a partial Σ-algebra, then A^{∗} satisfies H if, and only if, A (strongly) satisfies H_{∗}. A has to satisfy the definedness requirements implied by H_{∗} in order for A^{∗} to satisfy H. For example, if p^{a}(x),p^{b}(y) → r^{f} (x,y) is a clause in H, the corresponding clause in H_{∗} will be a≈x,b≈y → f(x)≈y. In order for A^{∗} to satisfy p^{a}(x),p^{b}(y) → r^{f} (x,y), f_{A}has to be defined on a_{A} with f_{A}(a_{A}) = b_{A}.

Theorem 7.2 Let H be a set of Σ^{∗}-clauses with S(K^{∗}) ⊆ H ⊆ \overline{S}(K^{∗}). Then H_{∗} is a stably local presentation of the quasi-variety K.

Proof. First we show that the class of algebras satisfying H_{∗} coincides with K. If A ⊧ H_{∗} then A^{∗} ⊧ H, and therefore, A^{∗} is in \overline{S}(K^{∗}). Hence A can be weakly embedded into an K-algebra B. In other words, A is isomorphic to a K-subalgebra, hence is a K-algebra itself.

Conversely, suppose that A is in K. Then A^{∗} is in S(K^{∗}), so that A^{∗} ⊧ H, hence, A ⊧ H_{∗}.

Now we show that H_{∗} is stably local. According to Theorem 6.4 we have to show that every finite partial H_{∗}-algebra A weakly embeds into H_{∗}. Let such an algebra A be given. As A^{∗} ⊧ H and as H ⊆ \overline{S}(K^{∗}), the embedding property for A follows. □

Conversely, from a local theory K we can obtain a finite axiomatization H_{K} satisfying S(K^{∗}) ⊆ H_{K} ⊆ \overline{S}(K^{∗}). We may assume that K is flat and linear. (Otherwise, applying Proposition 4.1, we may replace K by K_{flin}, with K_{flin} the set of flat and linear instances of K.) Now define H_{K} to be the union of K^{∗} and the set of uniqueness clauses r^{f} (x_{1},... ,x_{n},y),r^{f} (x_{1},... ,x_{n},z) → y≈z for the relations.

Theorem 7.3 With H_{K} as defined above, if K is a local theory, then S(K^{∗}) ⊆ H_{K} ⊆ \overline{S}(K^{∗}).

Proof. Clearly, all full substructures of K^{∗} satisfy H_{K}. Moreover, if A^{∗} ⊧ H_{K}, then A is in particular a partial Kalgebra. By Theorem 6.1, any such A weakly embeds into K, hence A is in \overline{S}(K^{∗}). □

8 Conclusion and Further Remarks

In this paper we have established close relationships between the approaches by Evans, Burris and McAllester to capture polynomial time computation in the context of uniform word problems. The criteria by Evans and Burris are essentially semantic, relating functional and relational models of given presentations. Local inference (McAllester’s approach) and stable locality (our variant of this concept) are notions which are more proof-theoretic in nature. It was interesting to see how closely related these approaches are. We have shown that both Evans’ and Burris’ criteria lie in between the two variants of locality. The inclusions are proper (at least for Evans’ approach, for Burris’ we do not know yet). In particular the concept of stably local theories subsumes Burris’ method (which in turn subsumes Evans’ method), and the subsumption is strict for the Evans case.

8.1 Explicit Definedness Predicates

The reason why [stable] locality and the other two approaches are not quite equivalent is intimately related to the definedness requirements for partial functions that partial K-algebras or full substructures of K^{∗} have to satisfy. For the subclass of presentations for which the definedness requirements are void, we were able to establish equivalence of locality and Evans’ criterion. Definedness, however, is a semantic concept that is not so easily captured syntactically. Only those clauses for which the antecedent is satisfiable contribute to definedness properties.

The following approach should work to simulate some of these effects in the framework of stable locality. Transform any given K by replacing clauses such as s≈t → f(u)≈g(v) by (read “D(x)” as “x is defined”)

D(s),D(t),D(u),D(g(v)),s≈t → D(f(u))
D(s),D(t),D(u),D(f(u)),s≈t → D(g(v))
D(s),D(t),D(f(u)),D(g(v)),s≈t → f(u)≈g(v)

internalizing the notion of satisfaction for partial algebras. (The general case of the transformation should be obvious.) Let K^{D} denote the result of that transformation. Call K “Evans”-local if for every ground clause C = Γ → e we have K^{D}[C] ∪ Γ ∪ D[C] ⊧ e whenever K ⊧ C, with D[C] the set of facts D(t), for each subterm t in C and constant t in K. Like in stable locality, we may use substitution instances of theory clauses where variables are sent to subterms of C or constants in K. However, because of using the transformed clauses, we may additionally only compute with those terms in K_{[C]}that are semantically equal to a subterm of the query or to a constant in K. Int′ is an example of a presentation that is Evans-local.

Evans-locality should be equivalent to Evans’ criterion, but since its definition is somewhat awkward and since it is not clear how to design good recursively enumerable approximations of the concept, we have not yet investigated this claim in more detail.

8.2 Applications

It might be possible to exploit the relation between the semantic and proof-theoretic concepts for mutually transferring further techniques. In particular, certain (yet to be established) amalgamation properties for algebras would induce combination results for local theories over disjoint vocabularies.

Let P be any partial K-algebra. Let T (P) = T_{Σ}(P)/E_{P}, that is, the free (total) Σ-term algebra generated over P, modulo the congruence E_{P} generated by the identities in P, that is, the equations a_{0}≈f(a_{1},... ,a_{n}) such that a_{i} is in P and a_{0} = f_{P}(a_{1},... ,a_{n}) holds in P. We can turn T (P) into a K-algebra by dividing by the intersection K of all kernels of homomorphisms h: T (P) → A ∈ K. Let F (P,K) = T (P)/K. A specific case of a much more general result proved by Burmeister (1986) is this universal property of F (P,K):

Theorem 8.1 (Burmeister 1986) F (P,K) is a Kalgebra, and for any weak homomorphism h from P into a K-algebra B there is a unique homomorphism \overline{h}: F (P,K) → B such that h = \overline{h}∘ π, with π : P → F (P,K) the canonical weak homomorphism sending any element of P to its congruence class under K.

The theorem asserts that F (P,K) is the free (total) Kalgebra generated by the partial Σ-algebra P.

Corollary 8.2 If P weakly embeds into K then the canonical weak homomorphism π : P → F (P,K) is injective.

Hence, whenever a partial algebra P weakly embeds into K it specifically also weakly embeds into its free extension F (P,K), a fact already observed by Evans (1951).

Suppose now that we have two flat, linear, and superficial local theories K_{1} and K_{2} over disjoint signatures Σ_{1} and Σ_{2} respectively. We want to show that the union K_{1}∪ K_{2} is also local. One way to do this is to utilize the methods in (Nelson & Oppen 1979) for combining decision procedures. An algebraic proof might be obtained via an amalgamation construction similar to the one given by Baader & Schulz (1998) for proving decidability of the combination of certain unification problems.

We need to show that every finite partial K_{1}∪K_{2}-algebra P weakly embeds into K_{1} ∪ K_{2}, and then apply the theorem 6.3, Given P, forget the operations in Σ_{2} and Σ_{1}, respectively, yielding a partial K_{1}-algebra P_{1} and a partial K_{2}-algebra P_{2}. As the given theories are local, these algebras weakly embed into the free constructions F (P_{1},K_{1}) and F (P_{2},K_{2}), respectively. We believe that one can now amalgamate F (P_{1},K_{1}) and F (P_{2},K_{2}) into a single K_{1}∪K_{2}- algebra into which P weakly embeds to, but the details have not been worked out yet.

Acknowledgments I am are grateful to Sergei Vorobyov for directing my attention to Burris’ paper and to Viorica Sofronie-Stokkermans for fruitful discussions.

References

Baader, F. & Schulz, K. (1998), ‘Combination of constraint solvers for free and quasi-free structures’, Theoretical Computer Science 192, 107–161.

Bachmair, L. & Tiwari, A. (2000), Abstract congruence closure and specializations, in D. McAllester, ed., ‘Automated Deduction – CADE-17, 17th International Conference on Automated Deduction’, LNAI 1831, Springer-Verlag, Pittsburgh, PA, USA, pp. 64–78.

Basin, D. & Ganzinger, H. (2001), ‘Automated complexity analysis based on ordered resolution’, J. Association for Computing Machinery 48(1), 70–109.

Burmeister, P. (1986), A Model Theoretic Approach to Partial Algebras. Introduction to Theory and Application of Partial Algebras, Part. 1, Akademie-Verlag, Berlin.

Burris, S. (1995), ‘Polynomial time uniform word problems’, Mathematical Logic Quarterly 41, 173–182.

Cosmadakis, S. (1988), ‘The word and generator problem for lattices’, Information and Computation 77, 192– 217.

Dowling, W. F. & Gallier, J. H. (1984), ‘Linear-time algorithms for testing the satisfiability of propositional Horn formulae’, J. Logic Programming 3, 267–284.

Downey, P. J., Sethi, R. & Tarjan, R. E. (1980), ‘Variations on the common subexpressions problem’, J. Association for Computing Machinery 27(4), 771–785.

Evans, T. (1951), ‘The word problem for abstract algebras’, J. London Math. Soc. 26, 64–71.

Freese, R. (1989), ‘Finitely presented lattices: canonical forms and the covering relation’, Trans. Amer. Math. Soc. 312, 841–860.

Ganzinger, H. & McAllester, D. (2001), A new metacomplexity theorem for bottom-up logic programs, in ‘Proc. International Joint Conference on Automated Reasoning’, Lecture Notes in Computer Science, Springer-Verlag. To appear.

Ganzinger, H., Nieuwenhuis, R. & Nivela, P. (1994), The Saturate system. System available at http://www.mpisb.mpg.de/SATURATE/.

Givan, R. & McAllester, D. (1992), New results on local inference relations, in ‘Principles of Knowledge Representation and reasoning: Proceedings of the Third International Conference (KR’92)’, Morgan Kaufmann Press, pp. 403–412.

Knuth, D. & Bendix, P. (1970), Simple word problems in universal algebras, in J. Leech, ed., ‘Computational Problems in Abstract Algebra’, Pergamon Press, Oxford, pp. 263–297.

Kozen, D. (1977), Complexity of finitely presented algebras, in ‘Proc. 9th STOC’, pp. 164–177.

McAllester, D. (1993), ‘Automatic recognition of tractability in inference relations’, J. Association for Computing Machinery 40(2), 284–303.

McAllester, D. (1999), On the complexity analysis of static analyses, in A. Cortesi & R. Filé, eds, ‘Static Analysis — 6th International Symposium, SAS’99’, LNCS 1694, Springer-Verlag, Venice, Italy, pp. 312–329.

Nelson, G. & Oppen, D. C. (1979), ‘Simplification by cooperating decision procedures’, ACM Transactions on Programming Languages and Systems 2(2), 245–257.

Scott, D. (1979), Identity and existence in intuitionistic logic, in M. Fourman, ed., ‘Durham proceedings (1977), Applications of Sheaves’, Vol. 753 of Lecture Notes in Mathematics, Springer Verlag, pp. 660–696.

Skolem, T. (1920), ‘Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischer Sätze nebst einem Theorem über dichte Mengen’, Skrifter utgitt av Videnskapsselskapet i Kristiania I(4), 1–36. Also in: Th. Skolem, Selected Works in Logic (Jens Erik Fendstad, ed.), Scand. Univ. Books, Universitetsforlaget, Oslo, 1970, pp. 103–136.