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é): : \neg p \lor \neg q \lor \cdots \lor \neg t \lor u. Hornovu klauzuli tak lze obecně zapsat jako implikaci ve formě: : (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.

Logické programování

Hornovy klauzule mají stěžejní roli v logickém programování (např. v jazyce Prolog) a jsou důležité pro konstruktivní logiku.

Hornova klauzule obsahující právě jeden pozitivní literál a několik (nejméně jeden) negativních, vyjadřuje implikaci. Někdy se označuje jako určitá klauzule, v jazyce Prolog odpovídá pravidlu (A :- B1, B2, . +more, Bn. ). Klauzule obsahující pouze jeden pozitivní literál a žádné negativní odpovídá prostému tvrzení. Někdy se označuje jako cílová klauzule, v jazyce Prolog odpovídá faktu (A :- true. , případně prostě A. ). Klauzule neobsahující žádný pozitivní literál a obsahující několik negativních odpovídá v jazyce Prolog dotazu (. - B1, B2, . , Bn. ).

Reference

Kategorie:Logika