Normal forms and syntactic completeness proofs for functional independencies

We prove normal form theorems of a complete axiom system for the inference of functional dependencies and independencies in relational databases. We also show that all proofs in our system have a normal form where the application of independency rules is limited to three levels. Our normal form results in a faster proof-search engine in deriving consequences of functional independencies. As a result, we get a new construction of an Armstrong relation for a given set of functional dependencies. It is also shown that an Armstrong relation for a set of functional dependencies and independencies do not exist in general, and this generalizes the same result valid under the closed-world assumption.

Authors

• Duminda Wijesekera
• M. Ganesh
• Jaideep Srivastava
• Anil Nerode

Keywords

• Completeness proofs
• Data mining
• Functional dependencies
• Integrity constraints