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 a lso show that all proofs in our system have a normal form where the applica tion of independency rules is limited to three levels. Our normal form resu lts in a faster proof-search engine in deriving consequences of functional independencies. As a result, we get a new construction of an Armstrong rela tion for a given set of functional dependencies. It is also shown that an A rmstrong relation for a set of functional dependencies and independencies d o not exist in general, and this generalizes the same result valid under th e closed-world assumption. (C) 2001 Elsevier Science B.V. All rights reserv ed.