Hornova klauzule

Ve výrokové logice se jako Hornova klauzule označuje speciální druh klauzule (disjunkce literálů), která obsahuje nejvýše jeden pozitivní literál (ostatní jsou negované):

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

Hornovu klauzuli tak lze obecně zapsat jako implikaci ve formě:

${\displaystyle (p\land q\land \cdots \land t)\implies u}$.

Jako Hornova formule se pak označuje formule v konjunktivní normální formě, která se skládá z Hornových klauzulí. Jako duální Hornova klauzule se pak označuje klauzule, která obsahuje nejvýše jeden negativní literál (a ostatní pozitivní).

Důležitost Hornových klauzulí spočívá v tom, že při omezení se na Hornovy klauzule místo obecných klauzulí můžeme v různých případech získat významné zrychlení inferenčních algoritmů. Například úloha rozhodnutí splnitelnosti obecné výrokové CNF formule je NP-úplná, ale splnitelnost konjunkce Hornových klauzulí lze vyřešit v lineárním čase. ^[1]