Логичко програмирање је парадигма програмирања на основу формалне логике. Програм написан на језику логичког програмирања је скуп реченица у логичком облику, изражавајући чињенице и правила о неком домену проблема. Главна породица логичког програмског језика укључује Пролог, одговор сет програмирање (ASP) и Даталог. У свим овим језицима, правила су написана у форми клаузула: H :- B1, …, Bn. и читају се декларативно као логичне последице: H if B1 и … и Bn. H се зове шеф правила и B1, …, Bn назива се тело. Чињенице су правила која немају тело, и записана у поједностављеном облику: H. У најједноставнијем случају у којем H, B1, …, Bn су све атомске формуле, те клаузуле се називају одређене клаузуле или Хорн клаузуле. Међутим, постоје многа проширења у овом једноставном случају, најважнији је случај у коме услови у телу клаузулом такође могу бити негативи атомских формула. Логички програмски језици који садрже овај додатак имају репрезентације знања могућности не-монотоне логике.
У АСП и Даталог, логички програми имају само декларативно читање, а њихово извршење врши се помоћу доказ поступка или модел генератора чије понашање није требало да буде под контролом програмера. Међутим, у Пролог породици језика, логички програми имају процедуралну интерпретацију као процедуру циља за смањење: да реши H, реши B1, и... и реши Bn.
Узмимо, на пример, следећу клаузулу: непоуздан(X) :- човек (X). заснована на пример користи Terry Winograd да илуструје програмски језик Planner. Као клаузула логике програма, може се користити и као поступак да се утврди да је X варљив тестирањем да ли је X човек, и као поступак да пронађе X који је непоуздан од проналажења X што је човек. Чак и чињенице имају процедурално тумачење. На пример, клаузула: човек (Сократ). се може користити и као поступак да покажу да је Сократ човек, и као процедура да пронађу X што је човек под "додељивањем" Сократ X.
Декларативно читање логичких програма може да се користи од стране програмера да провери исправност. Штавише, технике програмске трансформације логичке основе се такође могу користити за трансформацију логичких програма у логички еквивалентне програме који су ефикаснији. У Пролог породици логичких програмских језика, програмер може да користи за решавање познатог проблема понашање механизма извршења како би унапредио ефикасност програма.
Историја Употреба математичке логике да се представе и изврше рачунарски програми је такође одлика ламбда рачуна, коју је развио Alonzo Church у 1930. Међутим, први предлог да се користе клаузулне форме логике за заступање рачунарских програма је направио Cordell Green.Cordell Green. Ово се користило за аксиоматизацију подгрупе Lisp-а, заједно са представом улазно-излазних односа, да израчуна однос симулацијом извршења програма у Lisp-у. Foster и Elcock's Absys, с друге стране, примењују комбинацију једначина и ламбда рачуна у асертионал програмском језику који не поставља никаква ограничења на редослед којим се обављају операцијеJ.M. Foster and E.W. Elcock.
Логичко програмирање у садашњем облику може се пратити уназад до расправе у касним 1960-им и раних 1970-их о декларативном односу процедуралне репрезентације знања и вештачке интелигенције. Заговорници декларативне репрезентације су посебно радили на Stanford-у, у вези са John McCarthy, Bertram Raphael и Cordell Green, и у Edinburgh, са John Alan Robinson (академски посетилац из Syracuse University), Pat Hayes, и Robert Kowalski. Заговорници процедуралних репрезентација су углавном центрирани на MIT-у, под вођством Марвина Минског и Симора Паперта.
Иако је заснован на доказу метода логике, планер, развијен на МИТ-у, био је први језик који се појављује у овом процедуралист парадигме.Carl Hewitt. Планер је истакнут образац-директно призивање процедуралних планова из циљева (тј циљ за смањење или назад везивање) и од тврдњи (тј напред уланчавање). Најутицајнији имплементатор Планера је подскуп Планера, назван Микро-Планер, који су реализовали Gerry Sussman, Eugene Charniak и Terry Winograd. Коришћен је за спровођење Winograd природног језика разумевања програма SHRDLU, који је био прекретница у то време. Да би се изборио са веома ограниченим меморијским системима у то време, планер је користио одустајање контролне структуре, тако да је само један могући прорачунат пут морао да се чува у исто време. Планер је довео до програмских језика QA-4, Popler, Conniver и QLISP.
Хејс и Ковалски у Единбургу су покушали да помире логику базирану на декларативни приступ представљања знања са Планеровом процедуралном екипом. Хејс (1973) је открио језик, Golux, у којима различити поступци могу се добити променом понашања теореме.Pat Hayes. Ковалски, с друге стране, развио је СЛД резолуцију,Robert Kowalski Predicate Logic as a Programming Language Memo 70, Department of Artificial Intelligence, Edinburgh University. 1973. варијанта СЛ-резолуцијеRobert Kowalski and Donald and Kuehner . Ковалски је сарађивао са Colmerauer у Марсељу, који је развио ове идеје у дизајну и имплементацији програмског језика Пролог.
Удружење за логичко програмирање је основано да промовише логичко програмирање у 1986.
Пролог је довео до програмских језика ALF, Fril, Gödel, Mercury, Oz, Ciao, Visual Prolog, XSB, и λProlog, као и низ логичких упоредних програмских језика,принудни логички програмирамски језици и даталог.
Концепти
Логика и контрола Логичко програмирање се може посматрати као контрола одбијања. Важан концепт логичког програмирања је раздвајање програма у њихову логичку компоненту и њихова контрола компоненте. Са чистих логичких програмских језика, логичка компонента сама одређује решења производа. Контрола компоненте може да варира у обезбеђивању алтернативног начина извршења логичког програма. Овај појам је заробљен од стране слогана Алгоритам = Логика + Контрола где "Логика" представља логички програм и "контрола" представља различите стратегије теорема-доказивања.
Решавање проблема У поједностављеном, претпостављен случај у којем логички програм и врхунски атомски циљ не садрже променљиве, уназад образложење одређује се и-или дрво, које чини претраживање простора за решавање тог циља. Циљ највишег ниова је корен дрвета. С обзиром на било који чвор у дрвету и било које клаузуле чији је начелник одговар чвора, постоји низ детета чворова одговара под-циљева у телу клаузуле. Ова деца чворова су груписана заједно са "и". Алтернативни комплети деце одговарају алтернативним начинима решавања чворова и груписани су заједно са "или".
Свака стратегијска претрага може да се користи за претраживање овог простора. Пролог користи секвенцијалну, последњи-у-првом-испаду, стратегију одустајања, у којој само један алтернативни и један под-циљ се сматра истовремено. Остале стратегије претраге, као што су паралелне потраге, интелигентно одустајање, или најбоље прве потраге за налажење оптималног решења, такође су могуће.
У општем случају, где подциљеви деле варијабле, друге стратегије могу да се користе, као што је избор подциља да је веома инстанциран или да је довољно инстанциран тако да га само један поступак примењује. Такве стратегије се користе, на пример, у упоредном логичком програмирању.
Негација као неуспех За већину практичних примена, као и за апликације које захтевају немонотоно образложење у вештачкој интелигенцији, Хорн клаузула логичког програма треба да се прошири на нормалне логичке програме, са негативним условима. Клаузула у нормалном логичком програму има облик: H :- A1, …, An, не B1, …, не Bn. и декларативно се чита као логична импликација: H ако A1 и … и An и не B1 и … и не Bn. где H и све Ai и Bi су атомске формуле. Негирање у негативним литералима не Bi се обично назива "негација као неуспех", јер у већини имплементација, негативан услов не Bi је показао да држи показујући да је позитиван услов Bi не држи. На пример: лети(X) :- птица(X), није ненормално(X). ненормално(X) :- рањена(X). птица(Џон). птица(Мери). рањена(Џон). Даје циљ проналажења нечега што може да лети: :- лети(X). постоје два кандидата решења која решавају први подциљ птица(X), наиме X = Џон и X = Мери. Други подциљ није ненормално(Џон) првог кандидата решења није, зато што рањена(Џон) успиева и стога ненормално(Џон) успева. Међутим, други подциљ није ненормално(Мери) другог кандидата решења успева, зато што рањена(Мери) не успева и због тога ненормално(Мери) не успева. Дакле, X = Мери је једино решење циља.
Микро-планер има конструктор, под називом "thnot", којi, када се примењује на израз враћа вредност тачно, ако (и само ако) процена израза није тачна. Један еквивалентни оператор је нормално уграђен у модерној Пролог имплементацији . Обично је то написано каоне(циљ) или \+ циљ, где је циљ неки циљ (предлог) да се докаже у програму. Овај оператор се разликује од негације првог реда логике: негација као што је \+ X == 1 нетачна када је променљива X везан за атом1, али успева у свим другим случајевима, укључујући и када X је невезан. То чини Пролог образложење немонотоно X = 1, \+ X == 1 увек нетачно, док \+ X == 1, X = 1 може успети, везивање X у 1, зависно да ли је X првобитно везан (имајте на уму да стандардни Пролог извршава циљеве слево надесно).
Логично статус негације као неуспех био је нерешен све док Кејт Кларк показао да, под одређеним природним условима, то је тачно (а понекад и потпуно) имплементација класичне негације у односу на завршетак програма. Завршетак износи отприлике да у погледу скуп свих програмских клаузула са истим предикатима са леве стране, каже H :- Тело1. … H :- Телоk. као дефиниција предиката H акко (тело1 или … или телоk) где "акко" значи "ако и само ако". Писање завршетка такође захтева експлицитно коришћење предиката једнакости и укључивање низа одговарајућих аксиома за равноправност. Међутим, примена негације од неуспеха потребно је само ако половине дефиниција је без аксиома једнакости.
На пример, завршетак програма горе је: лети(X) акко птица(X), није ненормално(X). ненормално(X) iff рањена(X). птица(X) акко X = Џон или X = Мери. X = X. не Џон = Мери. не Мери= Џон . Појам завршетак радова је уско повезан са Макартијевим описивањем семантике за подразумевано резоновање, и на затвореном свету претпоставке.
Као алтернатива завршетка семантике, негација као неуспех може се тумачити епистемички, као и у стабилним моделима семантике као одговор сет програмирања. У овом тумачењу не(Bi) дословно значи да Bi се не зна или није веровао. Епистемичка тумачење имају ту предност да могу да се комбинују веома једноставно са класичном негацијом, као у "продуженом логичком програмирању", да озваничи такве фразе као што је "противно не може бити приказана", где је "у супротности" је класична негација и "не може бити приказано "је епистемичко тумачење негације као неуспех.
Представљање знања Чињеница да су Хорн клаузуле добиле процедурално тумачење и обрнуто, да се циљ процедуре смањења може схватити као Хорн клаузула + уназад расуђивање значи да логички програми комбинују декларативно и процедурално репрезентовање знања. Укључивање негације као неуспех значи да је логичко програмирање врста немонотоне логике.
Упркос својој једноставности у поређењу са класичном логиком, ова комбинација Хорн клаузуле и негације као неуспех се показала као изненађујуће изражајана. На пример, показано је да одговара, са неким даљим наставцима, сасвим природно језику полу-формалног законодавства. То је такође природни језик за изражавање здравог разума закона узрока и последице, као у ситуацији рачуна и догађаја рачуна.
Варијације и проширења
Пролог