On the decidability of the embedded multivalued dependency membership problem (database, automated deduction)
Bob P. Weems · 1985
The decidability of the membership problem for embedded multivalued dependencies (EMVDs) is an open problem in relational dependency theory. Given a set of EMVDs, determine if another EMVD holds in any relation where the set holds. A resolution-theoretic view is taken. The dependencies are viewed as clauses in Skolemized conjunctive normal form. Earlier work on the problem is recast in the resolution framework. A resolution based version of Sadri and Ullman's chase procedure is developed. This procedure extends the deletion feature of the original chase. An original top-down counterpart which includes factoring and deletes resolvents containing function terms is shown to be complete. Some previously known results are more easily proven from this procedure. Various results regarding axiom classes are given. In an attempt to find a smaller superclass than the template dependencies which contain the EMVDs and have a complete axiomatization, a canonical form for template dependencies is noted. It is shown that attempting to restrict the EMVDs by limiting the attributes in a partition produces no useful results.