Paper Info
Title
Unification and Matching Modulo Leaf-Permutative Equational Presentations
Abstract
Unification modulo variable-permuting equational presentations is known to be undecidable. We address here the problem of the existence of a unification algorithm for the class of linearvariable-permuting presentations, also known as leaf-permutativepresentations. We show that there is none, by exhibiting a leaf-permutative presentation whose unification problem is undecidable. We also exhibit one such presentation whose word and pattern matching problems are PSPACE-complete. The proof proceeds in three stages, by transforming length-preserving string-rewriting systems into atomic, then into bit-swappingstring-rewriting systems, and finally into leaf-permutative presentations.
Year
DOI
Venue
2008
10.1007/978-3-540-71070-7_30
IJCAR
Keywords
Field
DocType
equational presentation,unification algorithm,matching modulo leaf-permutative equational,length-preserving string-rewriting system,leaf-permutative presentation,linearvariable-permuting presentation,unification problem,bit-swappingstring-rewriting system,proof proceed,unification modulo,pattern matching
Discrete mathematics,Algebra,Binary strings,Modulo,Computer science,Word problem (mathematics education),Unification,Algorithm,Pattern matching,Undecidable problem,Equational theory
Conference
Volume
ISSN
Citations 
5195
0302-9743
0
PageRank 
References 
Authors
0.34
13
3
Name
Order
Citations
PageRank
Thierry Boy de la Tour112918.99
Mnacho Echenim29515.75
Paliath Narendran31100114.99