A Decision Algorithm for Stratified Context Unification
Manfred Schmidt-Schauß · Journal of Logic and Computation · 2002
Context unification is a variant of second‐order unification and also a generalization of string unification. Currently it is not known whether context unification is decidable. An expressive fragment of context unification is stratified context unification. Recently, it turned out that stratified context unification and one‐step rewrite constraints are equivalent. This paper contains a description of a decision algorithm SCU for stratified context unification together with a proof of its correctness, which shows decidability of stratified context unification as well as of satisfiability of one‐step rewrite constraints.