En lògica proposicional, una fórmula lògica és una clàusula de Horn si és una clàusula (disjunció de literals) amb, com a màxim, un literal positiu. Es diuen així pel lògic Alfred Horn, el primer a assenyalar la importància d'aquestes clàusules en 1951.^[1]

Això és un exemple d'una clàusula de Horn:

${\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}$

Una fórmula com aquesta també pot reescriure's de forma equivalent com una implicació:

${\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u}$

Una clàusula de Horn amb exactament un literal positiu és una clàusula "definite"; en àlgebra universal les clàusules "definites" resulten (apareixen) com quasi-identitats. Una clàusula de Horn sense cap literal positiu és de vegades anomeda clàusula objectiu (goal) o consulta (query), especialment en programació lògica.

Una fórmula de Horn és una cadena textual (string) de quantificadors existencials o universals seguits per una conjunció de clàusules de Horn.

La sintaxi d'una clàusula de Horn en PROLOG té el següent aspecte:

 filla(A,B) :- dona(A), pare(B,A).

que podria llegir-se així: "A és filla de B si A és dona i B és pare de A".

En termes lògics representa la següent implicació:

${\displaystyle (dona(A)\land pare(B,A))\to filla(A,B)}$

Per definició d'implicació s'obté la següent clàusula de Horn:

${\displaystyle \lnot dona(A)\lor \lnot pare(B,A)\lor filla(A,B)}$

Observe's que, en PROLOG, el símbol :- separa la conclusió de les condicions. En PROLOG, les variables s'escriuen començant per una lletra majúscula. Totes les condicions han de complir-se simultàniament perquè la conclusió siga vàlida; per tant, la coma (en algunes versions de PROLOG se substitueix la coma pel símbol &) que separa les diferents condicions és equivalent a la conjunció copulativa.

En canvi la disjunció normalment no es representa mitjançant símbols especials (encara que pot fer-se amb el símbol ;), sinó afegint regles noves al programa. En aquest cas:

 filla(A,B) :- dona(A), pare(B,A).
 filla(A,B) :- dona(A), mare(B,A).

que podrien llegir-se així: "A és filla de B si A és dona i B és pare d'A o A és filla de B si A és dona i B és mare d'A".

• Programació lògica

• Clàusula de Horn a PlanetMath (en anglés)