Normal forms and syntactic completeness proofs for functional independencies

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

Research output: Contribution to journalArticle


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.

Original languageEnglish
Pages (from-to)365-405
Number of pages41
JournalTheoretical Computer Science
Issue number1-2
Publication statusPublished - 6 Sep 2001
Externally publishedYes



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

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this