A clause in the matrix of a Prenex Normal Form formula is a first order Horn clause if:
- the prefix consists only of universal quantifiers quantifying over all variables in the clause
- the clause consists of a finite disjunction of positive or negative atoms with no more than one positive atom