Klauzula Horna

Klauzula Horna (ang. Horn clause) – klauzula, w której co najwyżej jeden element jest niezanegowany. Przykładami takich klauzul są {p,¬r,¬q} i {¬r,¬q}.

Klauzule Horna zapisuje się zwykle w postaci implikacyjnej:

• p ← r ∧ q
• ← r ∧ q

albo w prologowskiej:

• p :- r, q
• :- r, q

Klauzule Horna są używane w programowaniu logicznym (na przykład w Prologu). Wykorzystywane są również do reprezentowania wiedzy w systemach eksperckich, ponieważ spełniają ważną właściwość:

klauzula

$\neg p\lor \neg q\vee \ldots \vee \neg t\vee u$

jest równoważna

$(p\wedge q\wedge \ldots \wedge t)\to u$

Można wyróżnić trzy rodzaje klauzul Horna:

• klauzula pusta, niezawierająca literałów i oznaczająca prawdziwą wartość false, jest nazywana klauzulą zatrzymania,
• klauzula niezawierająca pozytywnego literału i zawierająca jeden lub więcej negatywnych literałów, jest nazywana klauzulą celu,
• klauzula zawierająca dokładnie jeden pozytywny literał i zero lub więcej negatywnych literałów, jest nazywana deklaracją procedury. Pozytywny literał określa się jako nazwa procedury, a negatywne literały to ciało procedury.

Zobacz też

• klauzula
• klauzula dualna