Hornova klauzule: Porovnání verzí

Přidáno 8 bajtů ,  před 10 měsíci
m
{{Autoritní data}}; formát zápisu šablon; kosmetické úpravy
Bez shrnutí editace
m ({{Autoritní data}}; formát zápisu šablon; kosmetické úpravy)
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 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|splnitelnostisplnitelnost]]i 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>{{citationCitation
| last1 = Dowling | first1 = William F.
| last2 = Gallier | first2 = Jean H.
 
{{Pahýl}}
{{Autoritní data}}
 
{{Portály|Matematika}}
 
1 404 608

editací