SFB 378 Einstiegsseite Postscript File BibTeX Entry

C
NEP

Inclusion Constraints over Non-Empty Sets of Trees

Author: Joachim Niehren and Martin Müller and Andreas Podelski

Editor: Max Dauchet

We present a new constraint system called Ines. Its constraints are conjunctions of inclusions $t_1\subseteq t_2$ between first-order terms (without set operators) which are interpreted over non-empty sets of trees. The existing systems of set constraints can express Ines constraints only if they include negation. Their satisfiability problem is NEXPTIME-complete. We present an incremental algorithm that solves the satisfiability problem of Ines constraints in cubic time. We intend to apply Ines constraints for type analysis for a concurrent constraint programming language.

SFB 378 Einstiegsseite Postscript File BibTeX Entry