• Home
• Teaching
• Research
• Publications

This paper considers, in a general setting, an axiomatic basis for Horn clause logic programming. 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-unification, quantitative deduction, and inheritance, in terms of two simple operators, and discusses algebraic properties these operators must satisfy. It develops fixpoint and model-theoretic semantics in this generalized setting, and shows that the fixpoint semantics is well-defined and coincides with the model-theoretic semantics. This leads to a generalized notion of a Horn clause logic program that captures a variety of fixpoint computations proposed in different guises, and allows concise expression in the logic programming idiom of several programs that involve aggregate operations.