Hornova klauzule: Porovnání verzí
m Robot: náhrada zastaralé matematické syntaxe podle mw:Extension:Math/Roadmap |
algoritmický význam Hornových klauzulí |
||
| Řádek 1: | Řádek 1: | ||
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é]]): |
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>. |
: <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ě |
Hornovu klauzuli tak lze obecně zapsat jako [[implikace|implikaci]] ve formě: |
||
: <math>(p \land q \land \cdots \land t) \implies u</math>. |
: <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í). |
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í == |
== Logické programování == |
||
Verze z 1. 7. 2021, 18:53
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é):
- .
Hornovu klauzuli tak lze obecně zapsat jako implikaci ve formě:
- .
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 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í splnitelnosti obecné výrokové CNF formule je NP-těžká, ale splnitelnost konjunkce Hornových klauzulí lze vyřešit v lineárním čase. [1]
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, ..., 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.).
- ↑ DOWLING, William F.; GALLIER, Jean H. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming. 1984, s. 267–284. DOI 10.1016/0743-1066(84)90014-1.