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 Horn envelope of a set of models. We provide polynomial algorithms for the recognition of whether a given functional dependency holds in a given Horn theory, as well as polynomial algorithms for the generation of some representative sets of functional dependencies that hold in a given Horn theory. We show that some functional dependencies inference problems are computationally difficult. We also study the structure of functional dependencies that hold in a Horn theory, show that every such functional dependency is in fact a single positive term Boolean function, and prove that for any Horn theory the set of its minimal functional dependencies is quasi-acyclic. Finally, we consider the problem of condensing a Horn theory, prove that any Horn theory has a unique condensation, and develop an efficient polynomial algorithm for condensing Horn theories.
Keywords: knowledge representation, Horn theory, functional
dependency, condensation, computational complexity, conjunctive normal
form, acyclic directed graph
Paper Available at:
ftp://dimacs.rutgers.edu/pub/dimacs/TechnicalReports/TechReports/1998/98-18.ps.gz
DIMACS Home Page