Хорнова клауза
 | Овај чланак је започет или проширен кроз пројекат семинарских радова. Потребно је проверити превод, правопис и вики-синтаксу. Када завршите са провером, допишете да након |проверено=. |
У математичкој логици и логичком програмирању, Хорнова клауза је логичка формула специфичне форме која даје корисне могућности за примену у логичком програмирању, формалној спецификацији и теорији модела. Име је добила по америчком математичару Алфреду Хорну.[1]
Дефиниција
[уреди | уреди извор]Хорнова клауза је клауза (дисјункција литерала) са највише једним позитивним, тј. ненегираним литералом.
Обрнуто, клауза са највише једним негираним литералом назива се двострука Хорнова клауза.
Хорнова клауза са тачно једним позитивним литералом је дефинитна клауза; дефинитна калузула без негираних литерала некада се назива и чињеница, док се Хорнова клауза без позитивних литерала некада назива и циљна клауза (приметимо да је празна клаузула једна циљна клаузула). Ова три типа Хорнових клауза илустрована су у следећој табели са исказним формулама:
| Дисјунктна форма | Импликацијска форма | Интуитивно се чита као | |
|---|---|---|---|
| Дефинитна клауза | ¬q1 ∨ ¬q2 ∨ ... ∨ ¬qn ∨ u | u ← q1 ∧ q2 ∧ ... ∧ qn | претпоставимо да, ако q1 и q2 и ... и qn важе, тада важи и u |
| Чињеница | u | u | претпоставимо да важи u |
| Циљна клауза | ¬q1 ∨ ¬q2 ∨ ... ∨ ¬qn | нетачно ← q1 ∧ q2 ∧ ... ∧ qn | показујемо да важи q1, q2, ..., qn |
У неисказном случају, све променљиве у клаузи су имплицитно универзално квантификоване у опсегу целе клаузе. Тако на пример:
- ¬ човек(X) ∨ смртан(X)
има значење:
- ∀X( ¬ човек(X) ∨ смртан(X) )
што је логички еквивалентно формули:
- ∀X ( човек(X) → смртан(X) )
Хорнове клаузе имају кључну улогу у интуитивној и рачунарској логици. Важне су и у аутоматском доказивању теорема методом резолуције, јер је резолуција две Хорнове клаузе једна Хорнова клауза, а резолуција циљне и дефинитне клаузуле је циљна клауза. Ове особине Хорнових клауза омогућава велику ефикасност у аутоматском доказивању теорема (представљених као негацијa циљне клаузе).
Исказне Хорнове клаузе имају улогу и у теорији комплексности. Проблем налажења валуације у којој је конјункција Хорнових клауза тачна је P-комплетан проблем, решив у линеарном времену,[2] који се некада назива ХОРНСАТ (Међутим, неограничени САТ проблем је НП–комплетан). Задовољивост Хорнових клауза првог реда је неодлучив задатак.
Логичко програмирање
[уреди | уреди извор]Хорнове клаузе представљају основу логичког програмирања, где је уобичајан запис дефинитних клауза у форми импликације:
- (p ∧ q ∧ ... ∧ t) → u
У ствари, чињеница да је резолуција циљне и дефинитне клаузе циљна клауза, представља основу за правило закључивања у СЛД резолуцији, која се користе за имплементацију логичког програмирања у програмском језику Пролог.
У логичком програмирању, дефинитна клауза се понаша као процедура за редукцију циља. На пример, Хорнова клауза из горњег примера понаша се као процедура:
- да се покаже да важи u, потребно је да се покаже да важе p, q, ... , t.
Како би се нагласила употреба клаузе у обрнутом редоследу, користи се запис:
- u ← (p ∧ q ∧ ... ∧ t)
У Прологу, ово се пише као:
u :- p, q, ..., t.
У логичком програмирању и Даталогу, израчунавање и оцена упита извршавају се тако што се негација проблема представи као циљна клауза. На пример, проблем решавања егзистенцијално квантификоване конјункције позитивних литерала:
- ∃X (p ∧ q ∧ ... ∧ t)
представља се као негација проблема, и записује преко логички еквивалентне циљне клаузе:
- ∀X (нетачно ← p ∧ q ∧ ... ∧ t)
У Прологу ово се пише као:
:- p, q, ..., t.
Решавање проблема своди се на доказивање контрадикције, која се преставља празном клаузом (или са „нетачно“). Решење проблема је супституција терма за променљиве у циљној клаузи, која се може добити из доказа контрадикције. Коришћене на овај начин, циљне клаузе сличне су конјунктивним упитима у релационим базама података, и логика Хорнових клауза еквивалентна је по експресивности Тјуринговим машинама.
Нотација у Прологу је заправо нејасна и термин „циљна клауза“ се некада двисмислено употребљава. Променљиве у циљној клаузи могу се сматрати и универзално и егзистенцијално квантификованим, а извођење у вредност „нетачно“ може се интерпретирати као извођење контрадикције, али и као иѕвођење успешног решавања проблема.
Ван Емден и Ковалски (1976) су истраживали својства теорије модела Хорнових клауза у контексту логичког програмирања, показујући да сцаки скуп дефинитних клауза D има јединствен минималан модел М. Атомичну формулу A логички имплицира D ако и само ако је A тачна у M. Из тога следи да је проблем P, представљнен као егзистенцијално квантификована конјукција позитивних литерала логички имлицира D ако и само ако је P тачно у M. Семантика минималног модела Хорнових клауза представља основу семантике стабилних модела логичких програма. [3]
Референце
[уреди | уреди извор]- ^ Horn, Alfred (1951). „On sentences which are true of direct unions of algebras”. Journal of Symbolic Logic. 16 (1): 14—21. doi:10.2307/2268661.
- ^ Dowling, William F.; Gallier, Jean H. (1984). „Linear-time algorithms for testing the satisfiability of propositional Horn formulae”. Journal of Logic Programming. 1 (3): 267—284. doi:10.1016/0743-1066(84)90014-1.
- ^ van Emden, M. H.; Kowalski, R. A. (1976). „The semantics of predicate logic as a programming language” (PDF). Journal of the ACM. 23 (4): 733—742. doi:10.1145/321978.321991.
Спољашње везе
[уреди | уреди извор]- Alex Sakharov. „Horn Clause”. MathWorld.