de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

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

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44474

Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Ganzinger, H. (2001). Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems. In D. A. Williams (Ed.), Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS-01) (pp. 81-90). Los Alamitos, USA: IEEE.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-3235-E
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.