%
% GENERATED FROM https://www.coli.uni-saarland.de
%    by   : anonymous
%    IP   : coli2006.lst.uni-saarland.de
%    at   : Mon, 05 Feb 2024 15:43:32 +0100 GMT
%    
% Selection : Reference #1037
%




@InProceedings{Niehren_et_al:1997_1,
      AUTHOR = {Niehren, Joachim and Pinkal, Manfred and Ruhrberg, Peter},
      TITLE = {On Equality up-to Constraints over Finite Trees, Context Unification and One-Step Rewriting},
      YEAR = {1997},
      BOOKTITLE = {14th International Conference on Automated Deduction (CADE 14), July 13-17},
      NUMBER = {1249},
      PAGES = {34-48},
      EDITOR = {McCune, W.},
      SERIES = {Lecture Notes in Computer Science},
      ADDRESS = {Townsville, Australia},
      PUBLISHER = {Springer},
      URL = {Full version available from http://www.ps.uni-sb.de/Papers/abstracts/fullContext.html},
      ABSTRACT = {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.},
      ANNOTE = {COLIURL : Niehren:1997:ECF.pdf Niehren:1997:ECF.ps}
}