Hornova klauzule

Z Wikipedie, otevřené encyklopedie
Skočit na: Navigace, Hledání

V logice, konkrétně 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 \or \neg q \or \cdots \or \neg t \or u.

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

(p \and q \and \cdots \and 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í).

Logické programování[editovat | editovat zdroj]

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, ..., 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.).