On functional dependencies in q-Horn theories

This paper studies functional dependencies in q-Horn theories, and discusses their use in knowledge condensation. We introduce compact model-based representations of q-Horn theories, analyze the structure of functional dependencies in q-Horn theories, and show that every minimal functional dependency in a q-Horn theory Σ can be expressed either by a single term or by a single clause. We also prove that the set of all minimal functional dependencies in Σ is quasi-acyclic. We then develop polynomial time algorithms for recognizing whether a given functional dependency holds in a q-Horn theory, which is represented either by a q-Horn CNF or as the q-Horn envelope of a set of models. Finally, we show that every q-Horn theory has a unique condensation, and can be condensed in polynomial time.