Hornova klauzule: Porovnání verzí

Přidáno 832 bajtů ,  před 11 měsíci
algoritmický význam Hornových klauzulí
m (Robot: náhrada zastaralé matematické syntaxe podle mw:Extension:Math/Roadmap)
(algoritmický význam Hornových klauzulí)
Ve [[výroková logika|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 [[negace|negované]]):
: <math>\neg p \lor \neg q \lor \cdots \lor \neg t \lor u</math>.
Hornovu klauzuli tak lze obecně zapsat jako [[implikace|implikaci]] ve formě:
: <math>(p \land q \land \cdots \land t) \implies u</math>.
 
Jako ''Hornova formule'' se pak označuje [[formule (logika)|formule]] v [[konjunktivní normální forma|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 jen 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 úlohla rozhodnutí [[Splnitelnost|splnitelnosti]] obecné výrokové [[Konjunktivní normální forma|CNF]] formule je [[NP (třída složitosti)|NP-těžká]], ale splnitelnost konjunkce Hornových klauzulí lze vyřešit v lineárním čase. <ref>{{citation
| last1 = Dowling | first1 = William F.
| last2 = Gallier | first2 = Jean H.
| doi = 10.1016/0743-1066(84)90014-1
| issue = 3
| journal = Journal of Logic Programming
| mr = 770156
| pages = 267–284
| title = Linear-time algorithms for testing the satisfiability of propositional Horn formulae
| volume = 1
| year = 1984}}</ref>
 
== Logické programování ==
Neregistrovaný uživatel