  where the formulas φ1, …, φn, ψ are all atomic. A universal Horn sentence (also known to the computer scientists as a Horn clause) is a sentence that consists of universal quantifiers followed by a quantifier-free Horn formula; it is said to be strict if no negation sign occurs in it (i.e. if it doesn’t come from a quantifier-free Horn formula of the third kind). 