Well-Nested Context Unification

Abstract. Context unification (CU) is the open problem of solving context equations for trees. We distinguish a new decidable variant of CU? well-nested CU ? and present a new unification algorithm that solves well-nested context equations in non-deterministic polynomial time. We show that minimal well-nested solutions of context equations can be composed from the material present in the equation (see Theorem 1). This property is wishful when modeling natural language ellipsis in CU.

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Jordi Levy, Joachim Niehren, Mateu Villaret
• Keywords: Automated Reasoning, CADE 2005, Context Equations, Context Unification, Well-nested Context Equations