Hornova klauzule je klauzule
s nejvýše jedním pozitivním (nikoli negovaným) literálem.
V dalším je P množina pozitivních (nikoli negovaných - bez „negatítka” (¬)) - literálů
a N množina negativních literálů - s „negatítkem” (¬)) v klasuli.
(|A| je mohutnost množiny A respective počet prvků seznamu.)
Typy Hornových klauzulí tedy jsou:
programové - |P| = 1
fakt - |N| = 0
pravidlo - |N| > 0
cíl - |P| = 0, |N| > 0
Klausule v prologovské notaci:
fakt:
p.
pravidlo:
p :- n1, n2, …, nj, …, nk.
cíl:
?- n1, n2, …, nj, …, nk.
Kde p je v klasické notaci positivní literál a nj negativní.