Polynomial-time implication problems for unary inclusion dependencies

Unary inclusion dependencies are database constraints expressing subset relationships. The decidability of implication for these dependencies together with embedded implicational dependencies, such as functional dependencies, are investigated. As shown by Casanova et al., the unrestricted and finite implication problems are different for the class of functional and unary inclusion dependencies; also, for this class and for any fixed k, finite implication has no k-ary complete axiomatization. For both of these problems, complete axiomatizations and polynomial-time decision procedures are provided: linear time for unrestricted implication and cubic time for finite implication. It follows that functional and unary inclusion dependencies form a semantically natural class of first-order sentences with equality, which although not finitely controllable, is efficiently solvable and docile. Generalizing from these results, it is shown that the interaction between functionaland inclusion dependencies characterizes: (1) unrestricted implication of unary inclusion and all embedded implicational dependencies; (2) finite implication of unary inclusion and all full implicational dependencies; (3) finite implication of unary inclusion and all embedded tuple-generating dependencies. As a direct consequence of this analysis, most of the applications of dependency implication are extended, within polynomial-time, to database design problems involving unary inclusion dependencies. Such examples are tests for lossless joins and tests for complementarity of projective views. Finally, if one additionally requires that