Generalized Horn Clause Programs

This paper considers, in a general setting, an axiomatic basis for Horn clause logic program-ming. It characterizes a variety of \Horn-clause-like " computations, arising in contexts such as deductive databases, various abstract interpretations, and extensions to logic programming involving E-unication, quantitative deduction, and inheritance, in terms of two simple opera-tors, and discusses algebraic properties these operators must satisfy. It develops xpoint and model-theoretic semantics in this generalized setting, and shows that the xpoint semantics is well-de ned and coincides with the model-theoretic semantics. This leads to a generalized notion of a Horn clause logic program that captures a variety of xpoint computations proposed in dif-ferent guises, and allows concise expression in the logic programming idiom of several programs that involve aggregate operations