@InProceedings{Niehren_et_al:1997_1,
AUTHOR = {Niehren, Joachim and Pinkal, Manfred and Ruhrberg, Peter},
TITLE = {On Equality upto Constraints over Finite Trees, Context Unification and OneStep Rewriting},
YEAR = {1997},
BOOKTITLE = {14th International Conference on Automated Deduction (CADE 14), July 1317},
NUMBER = {1249},
PAGES = {3448},
EDITOR = {McCune, W.},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Townsville, Australia},
PUBLISHER = {Springer},
URL = {Full version available from http://www.ps.unisb.de/Papers/abstracts/fullContext.html},
ABSTRACT = {We introduce equality upto constraints over finite trees and investigate their expressiveness. Equality upto constraints subsume equality constraints, subtree constraints, and onestep rewriting constraints. We establish a close correspondence between equality upto constraints over finite trees and context unification. Context unification subsumes string unification and is subsumed by linear secondorder unification. We obtain the following three new results. The satisfiability problem of equality upto constraints is equivalent to context unification, which is an open problem. The positive existential fragment of the theory of onestep rewriting is decidable. The $exists^*forall^*exists^*$ fragment of the theory of context unification is undecidable.},
ANNOTE = {COLIURL : Niehren:1997:ECF.pdf Niehren:1997:ECF.ps} }
