The independence property of a class of set constraints

Abstract

We investigate a class of set constraints that is used for the type analysis of con­current constraint programs. Its constraints are inclusions between first-order terms (without set operators) interpreted over non-empty sets of finite trees. We show that this class has the independence property. We give a polynomial algorithm for entailment. The independence property is a fundamental property of constraint systems. It says that the constraints cannot express disjunctions, or, equivalently, that negated conjuncts are independent from each other. As a consequence, the satisfiability of constraints with negated conjuncts can be directly reduced to entailment.