Declarative Logic Programming. Michael Kifer

      where a and all bi’s and cj’s are atoms. The atom a is the head of the rule (2.1) and the conjunction (list) b₁, …, bm, not c₁, …, not cn of literals is its body. If r denotes a rule, we write H(r) and B(r) for the head and the body of r, respectively. We extend this notation to programs and write H(P) and B(P) for the sets of heads and bodies of rules in a program P.

      We often write rules as a ← B, where a is an atom and B is a list of literals. For every list B = b₁, …, bm, not c₁, …, not cn of literals we define B⁺ = {b₁, …, bm} and B⁻ = {c₁, …, cn}, and we often specify a rule a ← B as a ← B⁺, not B⁻. We note a slight abuse of the notation here. The expression in the body, B⁺, not B⁻, is not a list but a pair of sets. Nevertheless, as all semantics of logic programs we consider in this chapter are insensitive to the order of literals in the bodies of rules, the notation gives all essential information about the rule it describes.

      If n = 0, rule (2.1) is a Horn rule and if m + n = 0, a fact. In the latter case, we omit ‘←’ from the notation, that is, we write a instead of a ←. A logic program (or just a program) is a collection of rules. A Horn program is a program consisting of Horn rules.