 First-order Horn clause

A first-order clause containing at most one positive first-order literal. A clause with exactly one positive literal is definite; with no positive literal it is a constraint or goal clause.