Una cláusula de Horn (o definida) es una disyunción de literales de los cuales uno, como mucho, es positivo.[4]

Una cláusula de Horn es una cláusula de la forma:

A₁ v ... v A_k ← B₁ ^ ... ^ B_n, con k=1 ó k=0 y n>=0.

donde A y B representan átomos.

Las cláusulas de Horn con k=1 y n>0 son reglas.

Las cláusulas de Horn con k=1 y n=0 son hechos.

Las cláusulas de Horn con k=0 y n>0 son objetivos.

En las cláusulas de programa (reglas o hechos):

A ← B₁ ^ ... ^ B_n, con n>=0

el átomo A es la cabeza y el conjunto de átomos B es el cuerpo.

Ejemplos de los diferentes tipos de cláusulas de Horn:

Regla: hermanas(X,Y)←mujer(X)  ^ mujer(Y) ^ padres(X,P,M) ^ padres(Y,P,M)

Hecho: mujer(ana) ←

Objetivo: ← hermanas(X, ana)