Paper: Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems (at LICS 2001)

Authors: Harald Ganzinger

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 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.

BibTeX

  @InProceedings{Ganzinger-RelatingSemanticand,
    author = 	 {Harald Ganzinger},
    title = 	 {Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {81--90},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }