© 2002 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Original Article |
A Decision Algorithm for Stratified Context Unification
1 Fachbereich Informatik, Johann Wolfgang Goethe-Universität, PoBox 11 19 32, D-60054 Frankfurt, Germany. E-mail: schauss{at}ki.informatik.uni-frankfurt.de
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.
Keywords: Unification; constraint solving; automated deduction; context unification; string unification
Received 25 November 1999.