@INPROCEEDINGS{Ganzinger-01-lics,
        AUTHOR	= {Ganzinger, H.},
        TITLE   = {Relating Semantic and Proof-Theoretic Concepts
for Polynomial Time Decidability
of Uniform Word Problems},
        YEAR    = 2001,
        BOOKTITLE          = {Proc.\ 16th IEEE Symposium on Logic in Computer Science},
	PAGES		   = {81--92},
	PUBLISHER          = {IEEE Computer Society Press},
        Abstract = {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 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, our notion of weak locality subsumes
both Evans' and Burris' method.},
}