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

Ganzinger, Harald

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

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

MPS-Authors

/persons/resource/persons44474

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

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

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: https://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.