There might be a special kind of Rule in the case where there are several Atoms in the Head and when these Atoms are also connected in a Disjunctive way. When they are connected in a conjunctive way, which means by a logical AND, then this Implication can be split in several single Rules that only have one Atom in the head. For example if there is H1 and H2 in the head, this means from the the body there can be implied H1 and also H2, so one can split these two Rules.
It is different if one considered the Disjunction in the header, there the Semantics and its Interpretation comes close to the reverse Implication. For example "if I see something" which is the body, "then the light is one or the sun is shining."
This means either that or the other one or both.
In general a Clause is a Disjunction of atomic or negated atomic Formulas. If it is an Clause with only at most one not negated Atom in the Header, it is a Horn Clause. A special Case is a definitive Clause where one has exactly one non negated Atom, because one can also have Horn Clauses with no not negated Atoms. So the header part of the implication is empty, which is also possible. On the other hand one has Facts which are Clauses of a single not negated Atom which states simply a Fact.
Another example is hasBrother of mother of x and y implies that x is the uncle of y. Here one has a special case where mother will be function symbol, so it is function of x and the mother of x has the brother of y and this is the uncle. This is a Horn Clause with a function Symbol.
Further if x is a man and x a woman then one can imply nothing, so the empty Set. This is Horn Clause which means that these both Classes man and woman are Disjunctive
Lastly, given a Fact that EVA is an AI, so the instance, the single Element EVA is a member of the set of all AIs.
Disjunction of several non-negated Atoms
A1 ∧ A2 ∧ ... ∧ An → H1 ∨ H2 ∨ ... ∨ Hm Body Head
reverse Implication, as e.g. "if I see something, then the light is on or the sun is shining"
Horn Clause Clause with at most one not negated Atom
¬p ∨ ¬q ... ∨ ¬t ∨ u can be written as p ∧ q ... ∧ t → u
Definite Clause: Clause with exactly one not negated atom
Fact: Clause of a single not negated atom
Person(x) → Woman(x) ∨ Man(x) (clause)
Man(x) ∧ hasChild(x,y) → Father(x) (definitive Clause)
hasBrother(mother(x), y) → isUncle(x,y) (with function Symbol)
Man(x) ∧ Woman(x) → (horn clause)