# Publication details

##
On Equality Up-to Constraints over Finite Trees, Context Unification and One-Step Rewriting

Joachim Niehren, Manfred Pinkal, Peter Ruhrberg

Proceedings of the International Conference on Automated Deduction, Vol. 1249 of Lecture Notes in Computer Science, pp. 34-48, Springer-Verlag, 1997

We introduce equality up-to constraints over finite trees and investigate their expressiveness. Equality up-to
constraints subsume equality constraints, subtree constraints,
and one-step rewriting constraints.
We establish a close correspondence between
equality up-to constraints over finite trees and context unification.
Context unification subsumes string unification and is subsumed by
linear second-order unification. We obtain the following
three new results.
The satisfiability problem of equality up-to constraints is
equivalent to context unification, which is an open problem.
The positive existential fragment of the theory of one-step
rewriting is decidable. The $exists^*forall^*exists^*$
fragment of the theory of context unification is undecidable.

Download PDF
Show BibTeX

@INPROCEEDINGS{ContextUnif:97,
title = {On Equality Up-to Constraints over Finite Trees, Context Unification and One-Step Rewriting},
author = {Joachim Niehren and Manfred Pinkal and Peter Ruhrberg},
year = {1997},
month = {"14-17"#jul},
publisher = {{Springer-Verlag}},
booktitle = {Proceedings of the International Conference on Automated Deduction},
series = {{Lecture Notes in Computer Science}},
volume = {{1249}},
pages = {{34-48}},
address = {{Townsville, Australia}},
note = {"Full version available from http://www.ps.uni-sb.de/Papers/abstracts/fullContext.html"},
}

Login to edit

Legal notice, Privacy policy