Functional dependencies in Horn theories

This paper studies functional dependencies in Horn theories, both when the theory is represented by its clausal form and when it is defined as the Hor n envelope of a set of models. We provide polynomial algorithms for the rec ognition of whether a given functional dependency holds in a given Horn the ory, as well as polynomial algorithms for the generation of some representa tive sets of functional dependencies. We show that some problems of inferri ng functional dependencies (e.g., constructing an irredundant FD-cover) are computationally difficult. We also study the structure of functional depen dencies that hold in a Horn theory, showing that every such functional depe ndency is in fact a single positive term Boolean function, and prove that f or any Horn theory the set of its minimal functional dependencies is quasi- acyclic. Finally, we consider the problem of condensing a Horn theory, prov e that any Horn theory has a unique condensation, and develop an efficient polynomial algorithm for condensing Horn theories. (C) 1999 Elsevier Scienc e B.V. All rights reserved.