Логичко програмирање

Логичко програмирање је парадигма програмирања на основу формалне логике. Програм написан на језику логичког програмирања је скуп реченица у логичком облику, изражавајући чињенице и правила о неком домену проблема. Главна породица логичког програмског језика укључује Пролог, одговор сет програмирање (ASP) и Даталог. У свим овим језицима, правила су написана у форми клаузула:

H :- B₁, …, B_n.

и читају се декларативно као логичне последице:

H if B₁ и … и B_n.

H се зове шеф правила и B₁, …, B_n назива се тело. Чињенице су правила која немају тело, и записана у поједностављеном облику:

H.

У најједноставнијем случају у којем H, B₁, …, B_n су све атомске формуле, те клаузуле се називају одређене клаузуле или Хорн клаузуле. Међутим, постоје многа проширења у овом једноставном случају, најважнији је случај у коме услови у телу клаузулом такође могу бити негативи атомских формула. Логички програмски језици који садрже овај додатак имају репрезентације знања могућности не-монотоне логике.

У АСП и Даталог, логички програми имају само декларативно читање, а њихово извршење врши се помоћу доказ поступка или модел генератора чије понашање није требало да буде под контролом програмера. Међутим, у Пролог породици језика, логички програми имају процедуралну интерпретацију као процедуру циља за смањење:

да реши H, реши B₁, и... и реши B_n.

Узмимо, на пример, следећу клаузулу:

непоуздан(X) :- човек (X).

заснована на пример користи Terry Winograd да илуструје програмски језик Planner. Као клаузула логике програма, може се користити и као поступак да се утврди да је X  варљив тестирањем да ли је X човек, и као поступак да пронађе X који је непоуздан од проналажења X што је човек. Чак и чињенице имају процедурално тумачење. На пример, клаузула:

човек (Сократ).

се може користити и као поступак да покажу да је Сократ човек, и као процедура да пронађу X што је човек под "додељивањем" Сократ X.

Декларативно читање логичких програма може да се користи од стране програмера да провери исправност. Штавише, технике програмске трансформације логичке основе се такође могу користити за трансформацију логичких програма у логички еквивалентне програме који су ефикаснији. У Пролог породици логичких програмских језика, програмер може да користи за решавање познатог проблема понашање механизма извршења како би унапредио ефикасност програма.

Историја

Употреба математичке логике да се представе и изврше рачунарски програми је такође одлика ламбда рачуна, коју је развио  Alonzo Church у 1930. Међутим, први предлог да се користе клаузулне форме логике за заступање рачунарских програма је направио Cordell Green. Ово се користило за аксиоматизацију подгрупе Lisp-а, заједно са представом улазно-излазних односа, да израчуна однос симулацијом извршења програма у Lisp-у. Foster и Elcock's Absys, с друге стране, примењују комбинацију једначина и ламбда рачуна у асертионал програмском језику који не поставља никаква ограничења на редослед којим се обављају операције

Логичко програмирање у садашњем облику може се пратити уназад до расправе у касним 1960-им и раних 1970-их о декларативном  односу процедуралне репрезентације знања и вештачке интелигенције. Заговорници декларативне репрезентације су посебно радили на Stanford-у, у вези са John McCarthy, Bertram Raphael и Cordell Green, и у Edinburgh, са John Alan Robinson (академски посетилац из Syracuse University), Pat Hayes, и Robert Kowalski. Заговорници процедуралних репрезентација су углавном центрирани на  MIT-у, под вођством Марвина Минског и Симора Паперта.

Иако је заснован на доказу метода логике, планер, развијен на МИТ-у, био је први језик који се појављује у овом процедуралист парадигме. Планер је истакнут образац-директно призивање процедуралних планова из циљева (тј циљ за смањење или назад везивање) и од тврдњи (тј напред уланчавање). Најутицајнији имплементатор Планера је подскуп Планера, назван Микро-Планер, који су реализовали Gerry Sussman, Eugene Charniak и Terry Winograd. Коришћен је за спровођење Winograd природног језика разумевања програма SHRDLU, који је био прекретница у то време. Да би се изборио са веома ограниченим меморијским системима у то време, планер је користио одустајање контролне структуре, тако да је само један могући прорачунат пут морао да се чува у исто време. Планер је довео до програмских језика QA-4, Popler, Conniver и QLISP.

Хејс и Ковалски у Единбургу су покушали да помире логику базирану на декларативни приступ представљања знања са Планеровом процедуралном екипом. Хејс (1973) је открио језик, Golux, у којима различити поступци могу се добити променом понашања теореме. Ковалски, с друге стране, развио је  СЛД резолуцију, варијанта СЛ-резолуције . Ковалски је сарађивао са Colmerauer у Марсељу, који је развио ове идеје у дизајну и имплементацији програмског језика Пролог.

Удружење за логичко програмирање је основано да промовише логичко програмирање у 1986.

Пролог је довео до програмских језика ALF, Fril, Gödel, Mercury, Oz, Ciao, Visual Prolog, XSB, и λProlog, као и низ логичких упоредних програмских језика,принудни логички програмирамски језици и даталог.

Концепти

Логика и контрола

Логичко програмирање се може посматрати као контрола одбијања. Важан концепт логичког програмирања је раздвајање програма у њихову логичку компоненту и њихова контрола компоненте. Са чистих логичких програмских језика, логичка компонента сама одређује решења производа. Контрола компоненте може да варира у обезбеђивању алтернативног начина извршења логичког програма. Овај појам је заробљен од стране слогана

Алгоритам = Логика + Контрола

где "Логика" представља логички програм и "контрола" представља различите стратегије теорема-доказивања.

Решавање проблема

У поједностављеном, претпостављен случај у којем логички програм и врхунски атомски циљ не садрже променљиве, уназад образложење одређује се и-или дрво, које чини претраживање простора за решавање тог циља. Циљ највишег ниова је корен дрвета. С обзиром на било који чвор у дрвету и било које клаузуле чији је начелник одговар чвора, постоји низ детета чворова одговара под-циљева у телу клаузуле. Ова деца чворова су груписана заједно са "и". Алтернативни комплети деце одговарају алтернативним начинима решавања чворова и груписани  су заједно са "или".

Свака стратегијска претрага може да се користи за претраживање овог простора. Пролог користи секвенцијалну, последњи-у-првом-испаду, стратегију одустајања, у којој само један алтернативни и један под-циљ се сматра истовремено. Остале стратегије претраге, као што су паралелне потраге, интелигентно одустајање, или најбоље прве потраге за налажење оптималног решења, такође су могуће.

У општем случају, где подциљеви деле варијабле, друге стратегије могу да се користе, као што је избор подциља да је  веома инстанциран или да је довољно инстанциран тако да га само један поступак примењује. Такве стратегије се користе, на пример, у упоредном логичком програмирању.

Негација као неуспех

За већину практичних примена, као и за апликације које захтевају немонотоно образложење у вештачкој интелигенцији, Хорн клаузула логичког програма треба да се прошири на нормалне логичке програме, са негативним условима. Клаузула у нормалном логичком програму има облик:

H :- A₁, …, A_n, не B₁, …, не B_n.

и декларативно се чита као логична импликација:

H ако A₁ и … и A_n и не B₁ и … и не B_n.

где H и све A_i и  B_i су атомске формуле. Негирање у негативним литералима  не B_i се обично назива "негација као неуспех", јер у већини имплементација, негативан услов не B_i је показао да држи показујући да је позитиван услов B_i не држи. На пример:

лети(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  првобитно везан (имајте на уму да стандардни Пролог извршава циљеве слево надесно).

Логично статус негације као неуспех био је нерешен све док Кејт Кларк [1978] показао да, под одређеним природним условима, то је тачно (а понекад и потпуно) имплементација класичне негације у односу на завршетак програма. Завршетак износи отприлике да у погледу скуп свих програмских клаузула са истим предикатима са леве стране, каже

H :- Тело₁.

…

H :- Тело_k.

као дефиниција предиката

H акко (тело₁ или … или тело_k)

где "акко" значи "ако и само ако". Писање завршетка такође захтева експлицитно коришћење предиката једнакости и укључивање низа одговарајућих аксиома за равноправност. Међутим, примена негације од неуспеха потребно је само ако половине дефиниција је без аксиома једнакости.

На пример, завршетак програма горе је:

лети(X) акко птица(X), није ненормално(X).

ненормално(X) iff рањена(X).

птица(X) акко X = Џон или X = Мери.

X = X.

не Џон = Мери.

не Мери= Џон .

Појам завршетак радова је уско повезан са Макартијевим описивањем семантике за подразумевано резоновање, и на затвореном свету претпоставке.

 Као алтернатива завршетка семантике, негација као неуспех може се тумачити епистемички, као и у стабилним моделима семантике као одговор сет програмирања. У овом тумачењу не(B_i) дословно значи да B_i се не зна или није веровао. Епистемичка тумачење имају ту предност да могу да се комбинују веома једноставно са класичном негацијом, као у "продуженом логичком програмирању", да озваничи такве фразе као што је "противно не може бити приказана", где је "у супротности" је класична негација и "не може бити приказано "је епистемичко тумачење негације као неуспех.

Представљање знања

Чињеница да су Хорн клаузуле добиле процедурално тумачење и обрнуто, да се циљ процедуре смањења може схватити као Хорн клаузула + уназад расуђивање значи да логички програми комбинују декларативно и процедурално репрезентовање знања. Укључивање негације као неуспех значи да је логичко програмирање врста немонотоне логике.

Упркос својој једноставности у поређењу са класичном логиком, ова комбинација Хорн клаузуле и негације као неуспех се показала као изненађујуће изражајана. На пример, показано је да одговара, са неким даљим наставцима, сасвим природно језику полу-формалног законодавства. То је такође природни језик за изражавање здравог разума закона узрока и последице, као у ситуацији рачуна и догађаја рачуна.

Варијације и проширења

Пролог

Програмски језик Пролог је развијен 1972. од стране Alain Colmerauer. Изашао је из сарадње између Colmerauer у Марсељу и Роберт Ковалски у Единбургу. Colmerauer је радио на разумевању природног језика, користећи логику да представи семантику и користи резолуцију за питања и одговоре . Током лета 1971. године, Colmerauer и Ковалски открили су да би клаузула облика логике могла да се користи за представљање формалне граматике и да је резолуција теорема провере могла да се користи за анализу. 

То је у следећем лето 1972. године, Ковалски, поново у сарадњи са Colmerauer, развио процедурално тумачење импликација. Ово двоструко декларативно / процедурално тумачење је касније постало формализовано у Пролог нотацији

H :- B₁, …, B_n.

које се може прочитати (и користити) и декларативно и процедурално. Такође је постало јасно да таква клаузула може бити ограничена на одређеним тачкама или Хорн клаузуле, где је H, B₁, …, B_n су све атомске логичке формуле, и то СЛ-резолуција ће бити ограничена (и уопштена) ка Луш или СЛД-резолуцији. Ковалсково процедурално тумачење и Луш су описани 1973. у меморандуму, објављен 1974. године.

Colmerauer, са Филипом Роуселом, користи ово двоструко тумачење одредби као основу за Пролог, који је реализован у лето и јесен 1972. Први Пролог програм, такође написан 1972. и спроведен у Марсељу, био је француски упитнички систем . Употреба Пролога као практичан програмски језик је дао велики замах развоја компајлера од стране Давида Варена у Единбургу 1977. Експерименти су показали да Единбург Пролог могже да се такмичи са брзином обраде других симболичних програмских језика као што је Lisp. Единбург Пролог постао је де факто стандард и снажно је утицао на дефиницију ИСО стандард Пролог.

Абдуктивно логичко програмирање

Абдуктивно логичко програмирање је наставак нормалног логичког програмирања који омогућује неке предикате, декларисани као абдуктивни предикати, да буде "отворен" или недефинисан. Клаузула у абдуктивном логичком програму има облик:

H :- B₁, …, B_n, A₁, …, A_n.

где је H је атомска формула која није абдуктивна. сви  B_i су литерали чији предикати нисуз абдуктивни и A_i је атомска форумула чији предикати јесу абдуктивни. Абдуктивни предикатимогу бити ограничени интегритетом ограничења, која може имати форму:

лажан :- B₁, …, B_n.

где су B_i произвољни литерали (дефинисани или абдуктивни, и атомски или негативни). На пример:

лети(X) :- птица(X), нормалан(X).

лажан:- нормалан(X), рањен(X).

птица(Џон).

птица(Мери).

рањен(Џон).

где је предикат нормалан абдуктиван.

Решавање проблема се постиже извођењем изражене хипотезе у смислу абдуктивног предиката и решења проблема које треба решити. Ови проблеми могу бити или запажања која треба објаснити (као у класичној абдукцији) или циљеве које треба решити (као у нормалном логичком програмирању). На пример, хипотеза нормалан(Мери) објашњава посматрање лети(Мери). Штавише, иста хипотеза подразумева једино решење X = Мери у циљу проналажења нечега што може да лети:

:- лети(X).

Абдуктивно логичко програмирање се користи за дијагнозу квара, планирања, обраду природног језика и машинског учења. Такође се користити за тумачење негације као неуспех као облик абдукције.

Металогичко програмирање

Јер, математичка логика има дугу традицију разликовања између објектног језика и метајезика, логичко програмирање такође омогућава програмирање на метанивоу. Најједноставнији металогички програм је такозвани "ванила" мета-преводилац:

   решити(тачно).
   решити((A,B)):- решити(A), решити(B).
   решити(A):- клаузула(A,B), решити(B).

где тачно представља празан везник, и клаузула(A,B) значи да је објектни ниво клаузула облик A :- B.

Металогичко програмирање омогућава објектни-ниво и виши ниво репрезентације да се комбинује, као у природном језику. Може се користити за имплементацију било које логике која је одобрена путем закључивања правила

Принудно логичко програмирање

Принудно логичко програмирање комбинује Хорн клаузуле логичког програмирања са ограниченим решавањем. Простире Хорн клаузуле дозвољавајући неке предикате проглашене ограниченим предикатима, да се јављају као речи у телу клаузула. Принудни логички програм је скуп клаузула у облику:

H :- C₁, …, C_n $\Diamond$ B₁, …, B_n.

где H и сви B_i су атомске формуле, и C_i су ограничења. Декларативно, такве клаузуле се читају као обичне логичке импликације:

H ако C₁ и … и C_n и B₁ и … и B_n.

Међутим, док су предикати у главама клаузула дефинисани од стране принудног логичког програма, који предикате у ограничењу су унапред дефинисани од стране неког специфичног домена модела-теоријске структуре или теорије.

Процедурално, субгоалс чији предикате су дефинисани програмом се решава гол-редукције, као у обичном логичко програмирање, али ограничења су проверени за задовољивости од домена специфичне ограничење-солвер, који спроводи семантику ограничење предиката. Почетни проблем је решен сводећи га на задовољив заједно ограничења.

Пратећи принудни логички програм представља играчку временске базе Џонове историје као наставник:

наставник(Џон, хардвер, T) :- 1990 ≤ T, T < 1999.

наставник(Џон, софтвер, T) :- 1999 ≤ T, T < 2005.

наставник(Џон, логика, T) :- 2005 ≤ T, T ≤ 2012.

ранг(Џон, инструктор, T) :- 1990 ≤ T, T < 2010.

ранг(Џон, професор, T) :- 2010 ≤ T, T < 2014.

Овде ≤ и < су ограничени предикати, са својим уобичајеним жељеним семантикама. Следећи циљ клаузула је да упита базе података да би сазнали када је  Џон предавао логику и био професор:

:- наставник(Џон, логика, T), ранг(Џон, професор, T).

Решење је 2010 ≤ T, T ≤ 2012.

Принудно логичко програмирање се користи за решавање проблема у областима као што су грађевинарство, машинство, дигиталне верификације кола, аутоматизовани распоред, контрола ваздушног саобраћаја и финансија. Тесно је повезано са абдуктивним логичким програмирањем.

Упоредно логичко програмирање

Упоредно логичко програмирање интегрише концепте логике програмирања уз упоредно логичко програмирање. Њен развој је дао велики подстицај у 1980. својим избором за језик у систем програмирања јапанске пете генерације пројекта (ФГЦС).

Упоредно логичко програмирање је скуп Хорн клаузуле  у облику:

H :- G₁, …, G_n | B₁, …, B_n.

Коњукција G₁, … , G_n се зове стража клаузуле, и | је оператор обавеза. Декларативно, чувани Хорн клаузуле се читају као обичне логичке импликације:

H ако G₁ и … и G_n и B₁ и … и B_n.

Међутим, процедурално, када постоји неколико клаузула чија глава H да гол у мечу онда сесве клаузуле извршавају паралелно, провере да ли њихови чувари G₁, … , G_n чекају.

На пример, следећа упоредна логика програма дефинише предикат мешање (лево, десно, спој), који се може користити за нано два списка лево и десно, комбинујући их у једну листу Мерге да чува редослед две листе лево и десно :

мешање ([], [], []).

мешање (лево, десно, спој) :- лево = [први | одмор] | спој = [први | кратак-спој], мешање (Rest, десно, кратак-спој).

мешање (лево, десно, спој) :- десно= [први | одмор] | спој= [први | кратак-спој], мешање (лево, одмор, кратак-спој).

Ево, [] представља празну листу, и [глава | реп] представља списак са првог елемента глава затим листу реп, као Пролог. (Обратите пажњу да је прва појава | у другом и трећем клаузулу списак градитеља, а друга појава | је оператор обавеза) Програм може да се користи, на пример, да се мешају листе[кец, краљица, краљ] и[1, 4, 2] позивајући се на гол клаузулу:

мешање([кец, краљица, краљ], [1, 4, 2], спој).

Програм ће недетерминистички генерисати једино решење, на пример спој= [кец, краљица, 1, краљ, 4, 2].

Вероватно, упоредно логичко програмирање је засновано на порукама доношења а самим тим и подлеже истој неодређености као и друге истовремене поруке заобилазећи системе, као што су глумци (види неодређености у истовременом израчунавању). Карл Хјуит  је тврдио да, упоредно логичко програмирање се не заснива на логици у смислу да рачунарски кораци се не могу логички закључити [Хјуит и Агха, 1988]. Међутим, у упоредно логичко програмирање, било који резултат престанка обрачунавања је логична последица програма, и сваки делимични резултат делимичног обрачунавања је логична последица програма, а остатак циљ (процес мрежа). Сходно томе, неодређеност у израчунавању указује на то да не могу све логичне посљедице програма да се закључе.

Упоредно принудно логичко програмирање

Упоредно принудно логичко програмирање комбинује принудно логичко програмирање и принудно логичко програмирање, користећи ограничења за контролу конкуренције. Клаузула може да садржи стражара, који је скуп ограничења која могу да блокирају примену клаузуле. Када су задовољни стражари неколико клаузула, истовремено ограничење логичког програмирања чини посвећен избор на употребу само једног.

Индуктивно логичко програмирање

Индуктивно логичко програмирање се бави генерализацијом позитивних и негативних примера у контексту предзнања: Машинско учење логичких програма. Недавни рад у овој области, комбинујући логичко програмирање, учење и вероватноће, довело је до новог поља статистичког релационог учења и вероватноће индуктивног логичког програмирања.

Логичко програмирање вишег реда

Неколико истраживача су проширили логичко програмирање са програмским функцијама вишег реда изведених из логике вишег реда , као што су предикатске варијабле. Такви језици укључују Пролог екстензије ХиЛог и λПролог.

Линеарно логичко програмирање

Заснивање логичког програмирања са линеарном логиком је резултат у дизајну логичких програмских језика који су знатно израженији од оних заснованих на класичној логици.  Хорн клаузуле програма могу само да представљају државну промену променом аргумената за предикате. У линеарном логичком програмирању, може се користити амбијентална линеарна логика да подрже промену стања.

Неки рани пројекти логичких програмских језика на основу линеарне логике укључују LO [Andreoli & Pareschi, 1991], Lolli, ACL, и Forum [Miller, 1996]. 

Објектно-оријентисано логичко програмирање

Ф-логика продужава логичко програмирање са објектима и оквирима синтаксе. Велики број система је засновано на Ф-логици, укључујући Flora-2, FLORID, и веома скалабилном комерцијалном систему Ontobroker.

Логталк проширује Пролог програмски језик са подршком за објекте, протокола и других ООП концепта. Високо преносиви, подржава већина стандардно-жалбених Пролог система као преводиоца.

Трансакција логичког програмирања

Трансакција логика је наставак логичког програмирања са логичком теоријом државних модификација ажурирања. Она има и модел-теоријску семантику и процедурални један. Имплементација подскупа трансакције логике је доступан у систему Флора-2. Други прототипови су такође доступни.

Види још

• САТ проблем
• Принудно логичко програмирање
• Даталог
• Функционално програмирање
• Индуктивно логичко програмирање
• Расплинута логика
• Парадигме програмирања
• R++
• Образложење система
• Релацијско програмирање
• Задовољивости

Литература

• Carl Hewitt. Procedural Embedding of Knowledge In Planner IJCAI 1971.
• Carl Hewitt. The repeated demise of logic programming and why it will be reincarnated What Went Wrong and Why: Lessons from AI Research and Applications. Technical Report SS-06-08. AAAI Press. March 2006.
• Dantsin, Evgeny; Eiter, Thomas; Gottlob, Georg; Voronkov, Andrei (2001). „Complexity and expressive power of logic programming”. Surv. 33 (3): 374—425. doi:10.1145/502807.502810. 
• Ulf Nilsson and Jan Maluszynski, Logic, Programming and Prolog

Главни извори

• Baral, Chitta; Gelfond, Michael (1994). „Logic programming and knowledge representation”. The Journal of Logic Programming. 19-20: 73—148. doi:10.1016/0743-1066(94)90025-6. 
• Kowalski, Robert A. (1988). „The early years of logic programming”. Communications of the ACM. 31: 38—43. S2CID 12259230. doi:10.1145/35043.35046. 
• Lloyd, J. W. (1987). Foundations of Logic Programming. (2nd edition) (Springer-Verlag).

Други извори

• John McCarthy. Programs with common sense Symposium on Mechanization of Thought Processes. National Physical Laboratory. Teddington, England. 1958.
• D. Miller, G. Nadathur, F. Pfenning, A. Scedrov. Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol. 51. стр. 125–157, 1991.
• Ehud Shapiro (Editor). Concurrent Prolog MIT Press. 1987.
• James Slagle. Experiments with a Deductive Question-Answering Program CACM. December 1965.

Спољашње везе

• Logic Programming Virtual Library entry
• Bibliographies on Logic Programming Архивирано на сајту Wayback Machine (4. децембар 2008)
• Association for Logic Programming (ALP)
• Theory and Practice of Logic Programming
• Logic programming in C++ with Castor
• Logic programming in Oz
• Prolog Development Center
• Racklog: Logic Programming in Racket