Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 6, December 2002: pp. 929-953

A Decision Algorithm for Stratified Context Unification

Manfred Schmidt-Schauß1

1Fachbereich Informatik, Johann Wolfgang Goethe-Universität, PoBox 11 19 32, D-60054 Frankfurt, Germany. E-mail: schauss@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

Table of Contents   Full-Text PDF (190 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement