A finite logical disjunction of atomic first-order formulas or their negations, normally understood to have all its free variables universally quantified. An empty logical disjunction is false. A Horn clause has at most one positive atom.
New to topics? Read the docs here!