Sciweavers

CSCLP
2006
Springer

Complexity of a CHR Solver for Existentially Quantified Conjunctions of Equations over Trees

13 years 7 months ago
Complexity of a CHR Solver for Existentially Quantified Conjunctions of Equations over Trees
Abstract. Constraint Handling Rules (CHR) is a concurrent, committed-choice, rule-based language. One of the first CHR programs is the classic constraint solver for syntactic equality of rational trees that performs unification. We first prove its exponential complexity in time and space for non-flat equations and deduce from this proof a quadratic complexity for flat equations. We then present an extended CHR solver for solving existentially quantified conjunctions of non-flat equations in the theory of finite or infinite trees. We reach a quadratic complexity by first flattening the equations and introducing new existentially quantified variables, then using the classic solver, and finally eliminating particular equations and quantified variables.
Marc Meister, Khalil Djelloul, Thom W. Frühwi
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where CSCLP
Authors Marc Meister, Khalil Djelloul, Thom W. Frühwirth
Comments (0)