Feature constraints with first-class features

Abstract

Feature Constraint Systems have been proposed as a logical data structure for constraint (logic) programming. They provide a record-like view to trees by identifying subtrees by keyword rather than by position. Their atomic constraints are finer grained than in the constructor-based approach. The recently proposed CFT [15] in fact generalizes the rational tree system of Prolog II. We propose a new feature constraint system EF which extends CFT by considering features as first class values. As a consequence, EF contains constraints like x[v]w where v is a variable ranging over features, while CFT restricts v to be a fixed feature symbol. We show that the satisfiability of conjunctions of atomic EF-constraints is NP-complete. Satisfiability of quantifier-free JEF-constraints is shown to be decidable, while the ∃*∀*∃* fragment of the first order theory is undecidable.