Inclusion Constraints over Non-empty Sets of Trees

Abstract. We present a new constraint system called INES. Its constraints are conjunctions of inclusions t1 t2 between rst-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 satis ability problem is NEXPTIME-complete. We present an incremental algorithm that solves the satis ability problem of INES constraints in cubic time. We intend to apply INES constraints for type analysis for a concurrent constraint programming language.

• Type: Conference
• Year: 1997
• Where: TAPSOFT
• Authors: Martin Müller, Joachim Niehren, Andreas Podelski
• Keywords: INES Constraints, Satis Ability Problem, Set Constraints, Software Engineering, TAPSOFT 1997