Hornova klauzule: Porovnání verzí

Přidáno 670 bajtů ,  před 15 lety
sloučení příspěvku, mírné rozšíření, aplikace v Prologu (s konfliktem)
Bez shrnutí editace
(sloučení příspěvku, mírné rozšíření, aplikace v Prologu (s konfliktem))
V [[logika|logice]], konkrétně ve [[výroková logika|výrokové logice]] znamenáse jako '''Hornova klauzule''' tvrzeníoznačuje speciální druh [[klauzule]] ([[disjunkce]] literálů), která obsahuje nejvýše jeden pozitivní literál (ostatní jsou typu[[negace|negované]]):
: <math>\neg p \or \neg q \or \cdots \or \neg t \or u</math>.
:(''p'' '''a''' ''q'' '''a''' ... '''a''' ''t'') '''implikuje''' ''u'',
Hornovu klauzuli tak lze obecně zapsat jako [[implikace|implikaci]] ve formě
kde počet tvrzení spojených pomocí '''a''' je libovolný (i nulový).
: <math>(p \and q \and \cdots \and t) \implies u</math>.
 
'Jako ''Hornova formule''' (Hornse formula)pak jeoznačuje logická[[formule (logika)|formule]] v [[konjunktivní normální forma|konjunktivní normální formě]], která se skládá z Hornových klauzulí. Jako ''duální''Duální Hornova klauzule''' (dual-Hornse clause)pak je Hornovaoznačuje klauzule, vekterá kteréobsahuje jenejvýše maximálnějeden negativní literál (a ostatní pozitivní).
Hornova klauzule disjunkcí literálů s maximálně jedním positivním
 
literálem (ostatní jsou negované). Hornova klauzule s právě jedním positivním
== Logické programování ==
literálem se nazývá
jeden ''negativní'' literál. Hornovy klauzule mají stěžejní roli v [[logické programování|logickém programování]] (např. v jazyce [[Prolog (programovací jazyk)|Prolog]]) a jsou důležité pro [[konstruktivní logikulogika|konstruktivní (constructive logic)logiku]].
'''určitá klauzule''' (definite clause) a pokud v ní není žádný positivní literál,
 
občas se, zejména v logickém programování, nazývá '''cílová klauzule''' (goal clause).
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 (<code>A :- B1, B2, ..., Bn.</code>). 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 (<code>A :- true.</code>, případně prostě <code>A.</code>). Klauzule neobsahující žádný pozitivní literál a obsahující několik negativních odpovídá v jazyce Prolog dotazu (<code>?- B1, B2, ..., Bn.</code>).
'''Hornova formule''' (Horn formula) je logická formule v konjunktivní normální formě, která se skládá z Hornových klauzulí. '''Duální Hornova klauzule''' (dual-Horn clause) je Hornova klauzule, ve které je maximálně
jeden ''negativní'' literál. Hornovy klauzule mají stěžejní roli v logickém programování a jsou důležité pro konstruktivní logiku (constructive logic).
 
{{Matematický pahýl}}