Complexity of a CHR solver for existentially quantified conjunctions of equations over trees.Reportar como inadecuado




Complexity of a CHR solver for existentially quantified conjunctions of equations over trees. - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 Universität Ulm 2 LIFO - Laboratoire d-Informatique Fondamentale d-Orléans 3 Fakultat fur Informatik. Universitat Ulm

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.





Autor: Marc Meister - Khalil Djelloul - Thom Fruehwirth -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados