On rewrite constraints and context unification

We show that stratified context unification, which is one of the most expressive fragments of context unification known to be decidable, is equivalent to the satisfiability problem of slightly generalized rewriting constraints. Key words: Automatic Theorem Proving; Theory of Computation; Unification; Rewrite Constraints.

• Type: Journal
• Year: 2000
• Where: IPL
• Authors: Joachim Niehren, Sophie Tison, Ralf Treinen
• Keywords: Context Unification, Expressive Fragments, IPL 2000, Satisfiability Problem