Horn

A horn clause is a member of the subset of first order languages. The horn clause subset is used by modern logicians to deliberately limit the expressive power of first order logic in order to use a more easily computable subset.

The name "Horn Clause" comes from the logician Alfred Horn, who first pointed out the significance of such clauses in 1951, in the article "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21.