First-order clause
= First-order clause
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.