The Free On-line Dictionary of Computing (30 December 2018):

Horn clause

    A set of atomic literals with at most one positive
   literal.  Usually written

   	L <- L1, ..., Ln
   or
   	<- L1, ..., Ln

   where n>=0, "<-" means "is implied by" and comma stands for
   conjuction ("AND").  If L is false the clause is regarded as
   a goal.  Horn clauses can express a subset of statements of
   first order logic.

   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.

   A definite clause is a Horn clause that has exactly one
   positive literal.

   (2000-01-24)