In the clausal form of logic, an expression of the form

This should be contrasted with the general form of clause if where A₁ … A_m are the alternative conclusions and B₁ … B_n are the joint conditions. A Horn clause is a special case of this general form in that it contains at most one conclusion.

Horn clauses were first investigated by the logician Alfred Horn. The majority of formalisms employed in computer programming bear greater resemblance to Horn clauses than to the more general form. The logic programming language Prolog is based upon the Horn clause subset of logic.