Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems

In this paper we compare three approaches to polynomial time decidability for uniform word problems for quasi-varieties. 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.