Source : Free On-Line Dictionary of Computing

Horn clause
     
         A set of {atomic literals} with at most one {positive
        literal}.  Usually written
     
        	L <- L1, ..., Ln
        or
        	<- L1, ..., Ln
     
        where n>=0.  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)