Za razliku od imperativne i funkcijske paradigme koje se, redom, oslanjaju na Turingov stroj i \lambda–račun, logičko programiranje temelji se na logici prvog reda ograničenoj s takozvanim Hornovim klauzulama. Važno svojstvo Hornovih klauzula je da predstavljaju formule koje se mogu interpretirati kao procedure i time efikasno implementirati na računalu. Još jedno važno svojstvo je da logikom prvog reda, ograničenom na Hornove klauzule, možemo izraziti sve Turing–izračunljive funkcije (za definiciju vidi [10]).

U srži logičkog programiranja leži rezolucija. To je metoda kojom se dokazuje valjanost formule tako da se pokaže da negacija formule nije ispunjiva. Rezolucija u logici sudova je potpuna metoda, što znači da može zamijeniti bilo koji deduktivni sistem. Još se početkom sedamdesetih godina shvatilo da rezolucija može biti interpreter za jezik logike prvog reda ograničen s Hornovim klauzulama. Tako je rođen prvi logički programski jezik opće namjene — Prolog. Prolog sadrži samo tri osnovna konstrukta: činjenice, pravila i upite. Skup činjenica čini bazu znanja koja, zajedno s pravilima, definira logički program. Možemo kratko reći da se programiranje u Prologu svodi na konstruiranje pravila i odgovarajuće baze znanja.

Primjerima logičkih (deklarativnih) programa obično se opisuju neke stablaste strukture (primjerice, obiteljsko stablo). Na žalost, većina jednostavnijih (i po našem mišljenju, potpuno nezanimljivih) primjera u Prologu su vezani uz obiteljska stabla. No, Prolog se koristi u implementaciji kompleksnijih modela u područjima umjetne inteligencije i ekspertnih sustava. Jedan zanimljivi eksperiment je IBM Watson koji u pozadini ima „ pattern matching” algoritme implementirane u Prologu. IBM Watson je sustav znanja koji može odgovarati na pitanja koja su postavljena u prirodnom jeziku. Taj sustav je 2011. godine pobijedio u kvizu Jeopardy! u SAD–u dvojicu tadašnjih rekordera (vidi primjerice: http://en.wikipedia.org/wiki/Watson_(computer) ).

Napomenimo da je Prolog, kao i većina drugih logičkih programskih jezika, namijenjen za simbolički račun, u kojemu se naglasak stavlja na transformacije matematičkih izraza koji su zadani nizom simbola. Takve transformacije čuvaju semantičko značenje izraza, pa je svaki rezultat, koji je posljedica takvih transformacija, egzaktan. Jednu vrstu ovakvih transformacija ćemo uvesti kada budemo definirali metodu unifikacije u logici prvog reda. Ovo je, ujedno, i glavna razlika između Prologa i, primjerice, Fortran–a ili MATLAB–a, programskih jezika koji su prvenstveno namijenjeni za numerički račun, unutar kojeg su u središtu pozornosti floating–point reprezentacija (ograničena aproksimacija) realnih brojeva i floating–point aritmetika.

Članak je podijeljen u tri točke. U prvoj točki se bavimo metodom rezolucije u logici sudova, u drugoj općom rezolucijom u logici prvog reda, te u trećoj programskim jezikom Prolog. Želimo još naglasiti da je ovaj članak zapravo skraćena verzija diplomskog rada [7]. Dokaze, koji su ovdje ispušteni, možete pronaći u navedenom diplomskom radu.

Logika sudova je odlučiva teorija. To znači da postoji algoritam koji za svaku formulu logike sudova u konačno mnogo koraka odlučuje je li ona valjana ili ne. Neki algoritmi odlučivanja su, primjerice, tablice istinitosti i semantička stabla (vid [9]). U ovoj točki predstavljamo još jedan algoritam odlučivanja — rezoluciju. Ovdje, na početku, želimo naglasiti da programski jezik Prolog koristi rezoluciju za logiku prvog reda. No, odlučili smo prvo predstaviti metodu rezolucije za logiku sudova kako bismo na jednoj vrlo jednostavnoj teoriji objasnili glavne ideje.

Rezolucija je jednostavno pravilo zaključivanja koje se iterativno primjenjuje na formulu u konjunktivnoj normalnoj formi, sve dok se ne dobije formula s određenim svojstvom. Kao i metoda semantičkih stabala, rezolucija je metoda opovrgavanja — da bismo dokazali da je formula valjana, dokazujemo da njena negacija nije ispunjiva.

Smatramo da je čitatelj upoznat s osnovnim pojmovima klasične logike sudova kao što su: alfabet, formula, interpretacija, istinitost formule za zadanu interpretaciju, relacija logičke posljedice, te s raznim vrstama formula (ispunjiva, valjana, oboriva i antitautologija). Svi detalji mogu se vidjeti, primjerice, u [9].

Pošto ćemo dosta koristiti pojmove vezane uz normalne forme, ovdje ćemo ponoviti njihove definicije. Literal je svaka propozicionalna varijabla ili njena negacija. Disjunkcija formula je svaka formula oblika A_{1}\vee \ldots \vee A_{n}, gdje su A_{i} proizvoljne formule. Sasvim analogno se definira pojam konjunkcije formula. Elementarna disjunkcija je svaka disjunkcija literala. Konjunktivna normalna forma je svaka konjunkcija elementarnih disjunkcija. U daljnjem tekstu često ćemo umjesto "konjunktivna normalna forma" pisati samo kratko "KNF".

Iz teorema o normalnim formama znamo da za svaku formulu F logike sudova postoji KNF G tako da vrijedi F\Leftrightarrow G. Važno je naglasiti da postoji algoritam polinomne vremenske složenosti koji za svaku formulu F određuje KNF G tako da vrijedi: formula F je ispunjiva ako i samo ako je formula G ispunjiva (vidi [5]).

U daljnjem tekstu promatrat ćemo skupovni zapis KNF. Taj zapis ćemo sada formalno definirati.

Klauzula odgovara jednoj elementarnoj disjunkciji, dok klauzalni oblik formule odgovara konjunkciji elementarnih disjunkcija, odnosno, formuli u konjunktivnoj normalnoj formi. Primijetimo da su barem dvije prednosti skupovnog zapisa: nema ponavljanja istih literala u jednoj klauzuli, te ne moramo razmišljati o poretku literala i klauzula.

Od sada pa nadalje za prikaz formule u klauzalnom obliku koristit ćemo skraćenu notaciju tako što ćemo ukloniti vitičaste zagrade, a negaciju literala ćemo prikazati crticom iznad samog literala. Na primjer, formulu \lbrace \lbrace p, r\rbrace , \lbrace \lnot q, \lnot p, q\rbrace , \lbrace p, \lnot p, q\rbrace \rbrace zapisujemo kao \lbrace pr, \bar{q}\bar{p}q, p\bar{p}q\rbrace.

Formulu u klauzalnom obliku možemo dodatno pojednostavniti uklanjanjem trivijalnih klauzula koje sada definiramo.

Sljedeći teorem naglašava zašto iz skupa klauzula možemo izostaviti trivijalne klauzule.

Sada definiramo pravilo rezolucije. Ako je l neki literal tada s l^{\mathsf{c}} označavamo suprotni literal.

Ako se dvije klauzule podudaraju na više od jednom paru komplemantarnih literala, tada je očito njihova rezolventa trivijalna. Zatim, lako je vidjeti da pravilo rezolucije čuva ispunjivost. Točnije, vrijedi sljedeći teorem.

Koristeći pravilo rezolucije sada navodimo metodu rezolucije za logiku sudova. Metodu ćemo navesti u formi algoritma. Ulazni podatak tog algortima je neki skup klauzula S, a izlaz algoritma je jedna od sljedećih poruka: skupS je ispunjiv, odnosno skupS nije ispunjiv.

Metoda rezolucije u logici sudova:
Ulaz: Skup klauzula S.
Neka je S_{0}= S.
Ponavljaj sljedeće korake:

Dakle, metoda rezolucije se sastoji od iterativne primjene pravila rezolucije na skup klauzula s ciljem da se dobije prazna klauzula \Box. Naime, znamo da pravilo rezolucije čuva ispunjivost, stoga, ako u jednom trenutku dobijemo rezolventu koja je prazna klauzula (sjetimo se da prazna klauzula nije ispunjiva), možemo zaključiti da početni skup klauzula S nije ispunjiv.

Metoda rezolucije se zaustavlja ako pronađemo rezolventu koja je prazna klauzula ili ako nam ponestane parova klauzula pomoću kojih možemo generirati nove rezolvente. Budući da imamo samo konačan broj različitih klauzula u početno zadanom skupu klauzula, zaključujemo da se metoda rezolucija zaustavlja za proizvoljan ulaz.

Sada nam je cilj istaknuti najvažnija svojstva metode rezolucije. To su teoremi adekvatnosti i potpunosti. Kako bismo točno mogli formulirati navedene teoreme, moramo definirati pojam potpunog, odnosno nepotpunog rezolucijskog stabla.

Metodu rezolucije možemo zapisati u obliku tzv. rezolucijskog stabla. Listovi stabla označeni su klauzulama iz S koje sudjeluju u metodi rezolucije, dok su unutarnji čvorovi označeni rezolventama. Kažemo da je takvo stablo dobiveno iz skupa klauzula S, odnosno da je to rezolucijsko stablo za S. Korijen stabla može biti označen bilo kojom rezolventom koja se može dobiti u nekom koraku metode rezolucije. To znači da u svakom koraku metode rezolucije možemo promatrati novo rezolucijsko stablo. Jasno, nas će zanimati samo ona stabla kojima je korijen označen praznom klauzulom. Takvo stablo ćemo nazivati potpuno rezolucijsko stablo. Inače ćemo reći da se radi o nepotpunom rezolucijskom stablu.

Vremenska složenost metode rezolucije nije tako očita kao kod, primjerice, tablica istinitosti. Ona se može mjeriti brojem različitih rezolventi koje se generiraju tijekom zaključivanja. Haken je 1985. godine dokazao da postoji niz valjanih formula F_{1},F_{2},\dots, takvih da opovrgavanje svake formule F_{i} zahtijeva generiranje barem c^{n} rezolventi, gdje je c\gt 1. Svaka od formula F_{i} izražava Dirichletov princip: ako i+1 predmet bilo kako rasporedimo u i kutija, tada barem jedna kutija sadrži barem dva predmeta. Dokaz se može naći u [2]. Dakle, metoda rezolucije ima eksponencijalnu vremensku složenost. Ovo je očekivano, jer je poznato da je problem valjanosti co–NP–potpun.

Jedna od primjena rezolucije u logici sudova je u Davis–Putnam–Logemann–Loveland algoritmu za rješavanje NP–potpunog problema ispunjivosti logičke formule poznatog kao problem SAT. Osim što ima povijesni značaj time što je bio prvi primjer NP–potpunog problema, problem SAT je ujedno i jedan od najistraživanijih problema u praksi. Moderne varijante Davis–Putnam–Logemann–Lovelandovog algoritma, starog više od pola stoljeća, i danas se koriste za njegovo rješavanje (vidi, primjerice, [5] i [6]).

Kao i rezolucija u logici sudova, rezolucija u logici prvog reda (naziva se i opća rezolucija) je, također, adekvatna i potpuna na skupu svih formula logike prvog reda. Međutim, ispostavlja se da takva rezolucija nije efikasna za implementaciju na računalu. U tu svrhu promatraju se razne restrikcije opće rezolucije. U ovoj točki bavimo se jednom od takvih restrikcija, i to onom koja je početkom sedamdesetih godina prošlog stoljeća rezultirala pojavom prvog logičkog programskog jezika Prolog. Riječ je o SLD–rezoluciji (eng. Selective Linear Definite clause resolution) kojom ispitujemo ispunjivost samo onih formula logike prvog reda koje se mogu izraziti pomoću Hornovih klauzula.

Hornove klauzule imaju svojstvo da se sastoje od najviše jednog pozitivnog literala, tj. literala bez negacije. Takve klauzule, osim deklarativne imaju i proceduralnu interpretaciju, odnosno, mogu se promatrati kao procedure i time efikasno implementirati na računalu. Osim toga, Hornove klauzule imaju izražajnu moć Turingova stroja, što znači da pomoću njih možemo izraziti sve Turing-izračunljive funkcije. SLD–rezoluciju zapravo možemo promatrati kao interpreter programskog jezika kojeg čini skup Hornovih klauzula.

Danas svaka varijanta rezolucije u logici prvog reda, pa tako i SLD–rezolucija, uključuje moćnu metodu unifikacije. Metoda unifikacije rješava problem podudaranja terma1 — za dana dva terma koji sadrže neke individualne varijable, treba pronaći, ako postoji, najjednostavniju supstituciju individualnih varijabli termima, takvu da nakon nje početna dva terma budu jednaka. Ovdje ćemo opisati takozvanu Martelli-Montanarijevu unifikaciju iz 1982. godine.

Za razliku od opće rezolucije, SLD–rezolucija nije potpuna na skupu svih formula logike prvog reda. Razlog je taj što Hornovim klauzulama ne možemo izraziti sve valjane formule logike prvog reda. S druge strane, SLD–rezolucija je potpuna kad se ograniči samo na Hornove klauzule. To znači da za svaku neispunjivu Hornovu klauzulu postoji izvod SLD–rezolucijom koji je prazna klauzula.

Dok je rezolucija u logici sudova imala svojstvo da staje s radom u konačno mnogo koraka za svaki ulaz, SLD-rezolucija (a time i opća rezolucija) nema to svojstvo. SLD–rezolucija može raditi vječno ako joj na ulaz damo formulu koja je ispunjiva. Ovo je posljedica činjenice da logika prvog reda nije odlučiva teorija (vidi [10]).

Na početku moramo odrediti oblik formula s kojima ćemo raditi. U uvodu smo spomenuli da će metoda unifikacije raditi određene supstitucije na formulama. To znači da je poželjno da se formule sastoje od univerzalnih kvantifikatora. Oni nam garantiraju da ćemo individualne varijable u formuli moći zamijeniti proizvoljnim termima. Smatramo da je čitatelj upoznat s pojmom preneksne normalne forme (definicija i primjeri se mogu vidjeti, primjerice, u [9]).

U ovom dijelu promatramo formule u preneksnoj konjunktivnoj normalnoj formi, i to one koje se sastoje samo od univerzalnih kvantifikatora. Individualne varijable ćemo općenito označavati s x, y, z\dots, a konstantske simbole s a, b, c \dots.

Za proizvoljnu formulu logike prvog reda želimo naći njezinu Skolemovu normalnu formu. Dok smo u logici sudova imali logičku ekvivalenciju između formule i njezinog klauzalnog oblika (odnosno konjunktivne normalne formule), u logici prvog reda očuvana je samo ispunjivost. O ovome govori Skolemov teorem, čiji dokaz možete vidjeti, primjerice, u [9].

Skolemov teorem na neki način govori da se formula u logici prvog reda može svesti na formulu logike sudova eliminacijom egzistencijalnih kvantifikatora i promatranjem samo Skolemove normalne forme. Upravo je eliminacija egzistencijalnih kvantifikatora razlog zašto se gubi logička ekvivalencija između formule F i njezine Skolemove normalne forme F'.

Prije opisa metode unifikacije uvedimo nekoliko definicija. Cilj nam je formalno definirati pojam instanciranja individualne varijable termom.

Supstitucije ćemo označavati s \lambda, \mu, \sigma, \theta, dok ćemo praznu supstituciju označavati s \epsilon. Supstitucije želimo provoditi na svim formulama.

Rezultat supstitucije očito ne mora biti izraz bez individualnih varijabli. Supstitucija može samo „preimenovati” individualne varijable. Takva je, primjerice, sljedeća supstitucija: \lbrace x\leftarrow y, z\leftarrow w\rbrace.

Sada definiramo jednu posebnu vrstu supstitucije koju ćemo koristiti u metodi unifikacije.

Očito ne možemo sve atomarne formule unificirati. To su, primjerice, one kojima se relacijski, odnosno, funkcijski simboli razlikuju. Također, ne možemo unificirati atomarne formule oblika p(x) i p(f(x)), budući da bilo koja supstitucija mora simultano supstituirati terme x i f(x).

Primjerice, problem unifikacije skupa atomarnih formula \lbrace p(f(x),g(y)),p(f(f(a)),g(z))\rbrace svodi se na ispitivanje sljedeće "jednakosti": p(f(x),g(y))=p(f(f(a)),g(z)). Očito je da se dvije atomarne formule mogu unificirati ako i samo ako se sastoje od istih relacijskih simbola i primaju jednak broj argumenata. Iz tog razloga govorit ćemo o skupu jednakosti terma za skup atomarnih formula, Primjerice, skup jednakosti terma za skup atomarnih formula \lbrace p(f(x),g(y)),p(f(f(a)),g(z))\rbrace je sljedeći skup: \lbrace f(x) = f(f(a)), g(y) = g(z)\rbrace.

Metoda unifikacije u svakoj iteraciji pokušava primijeniti određenu \textbf {transformaciju} na skup jednakosti terma. Zanimaju nas samo one transformacije koje čuvaju skup svih unifikatora, jer upravo te transformacije čuvaju i najopćenitiji unifikator. Definirajmo sada dvije takve transformacije:

Sada navodimo metodu unifikacije. Zapisujemo je u obliku algoritma.

Metoda unifikacije u logici prvog reda:
Ulaz: Skup jednakosti terma.
Izvršavaj sljedeće korake (1)–(4) dok god se jedan od njih može primijeniti. Ako u jednom trenutku dobijemo skup jednakosti terma sa svojstvom da su sve jednakosti oblika x = t, gdje je x individualna varijabla koja se ne pojavljuje više nigdje na lijevoj strani neke jednakosti, postupak se zaustavlja s porukom: skup jednakosti terma na izlazu je najopćenitiji unifikator za zadani skup jednakosti terma.

Postoji nekoliko razloga za uvođenje Hornovih klauzula. Prvi je činjenica da se Hornovim klauzulama mogu izraziti sve parcijalno rekurzivne funkcije (vidi [3]), a time i sve Turing–izračunljive funkcije. Drugi razlog je taj što se Hornove klauzule mogu interpretirati kao jednostavne procedure. Ako uzmemo u obzir još i činjenicu da je rezolventa Hornovih klauzula i dalje Hornova klauzula, iste postaju prikladne za implementaciju na računalu. Treći razlog tiče se činjenice da su Hornove klauzule jedna od najboljih restrikcija logike prvog reda s ovim svojstvima. Počnimo s definicijom Hornovih klauzula.

Ovdje koristimo simbol „ \leftarrow” kao oznaku za implikaciju, jer osim što formula ima deklarativnu interpretaciju (da bismo dokazali A, moramo dokazati B_{1},\dots,B_{n}), formulu možemo interpretirati kao proceduru koja se sastoji od niza naredbi: da bismo izračunali A, moramo izračunati B_{1},\dots,B_{n}. Ovo opravdava sljedeću definiciju u kojoj uvodimo osnovnu terminologiju koja se koristi u logičkom programiranju.

Dakle, program se sastoji od procedura i baza znanja. Programu postavljamo upite u obliku ciljnih klauzula, te ako program stane u konačno mnogo koraka, tada odgovor na upit predstavljaju supstitucije nastale unifikacijom ciljnih i programskih klauzula (odnosno procedura i baza znanja). Rad programa ćemo opisati SLD–rezolucijom. Definirajmo sada neke posebne vrste supstitucija koje će nam trebati.

Neka je dan program P, ciljna klauzula G\equiv\lnot G_{1}\lor\cdots\lor\lnot G_{n} i supstitucija korektnog odgovora \theta. Prema definiciji vrijedi P\Rightarrow\forall(\lnot G\theta), odnosno, P\Rightarrow\forall((G_{1}\land\cdots\land G_{n})\theta). Dakle, za bilo koju supstituciju \sigma, svaki model za program P ujedno je i model za formulu (G_{1}\land\cdots\land G_{n})\theta\sigma. Supstitucija \theta\sigma će predstavljati odgovor na upit, pa ćemo pomoću nje moći iskazati teoreme adekvatnosti i potpunosti ograničene sada samo na program.

Kao što smo bili već napomenuli, SLD–rezolucija je restrikcija opće rezolucije na Hornove klauzule, odnosno, na program, kao što ćemo vidjeti. Ime joj je izvedeno iz SL–rezolucije (eng. Selecitive Linear clause resolution), koja je adekvatna i potpuna na skupu svih formula logike prvog reda. Sada metodu SLD–rezolucije zadajemo u obliku algoritma.

SLD–rezolucija u logici prvog reda:
Ulaz: Program P i ciljna klauzula G.
Neka je G_{0} = G.
Ciljnu klauzulu — rezolventu G_{i+1}, izvodimo iz klauzula G_{i} i C_{i}\in P odabirom literala A_{i}^{j}\in G_{i} koji se može unificirati s glavom klauzule C_{i} pomoću najopćenitijeg unifikatora \sigma_{i}:
 

Metoda SLD–rezolucije očito ne staje s radom za svaki program P i ciljnu klauzulu G. Primjer takvog programa i ciljne klauzule predstavljaju sljedeće formule: p(x,z)\ \leftarrow p(x,y)\land p(y,z),\ \leftarrow p(a,b). Metoda je, također, nedeterministična u slučaju da ne definiramo pravila izračunavanja i pretraživanja.

Objasnimo sada na što se odnose riječi selective, linear i definite u nazivu SLD–rezolucije. Riječ „ selective" se odnosi na postojanje pravila izračunavanja. Jedno pravilo izračunavanja je, primjerice, pravilo LIFO („ last in, first out”). To pravilo izračunavanja za unifikaciju odabire literal koji je zadnji uveden u ciljnu klauzulu. Riječ „ linear" se odnosi na činjenicu da rezolucija generira niz ciljnih klauzula G_{0},G_{1},\dots, takvih da se u i–tom koraku, ciljna klauzula G_{i-1} odabire za podudaranje. Riječ „ definite" se odnosi na činjenicu da se rezolucija provodi samo nad Hornovim klauzulama.

Sada iskazujemo teoreme adekvatnosti i potpunosti za SLD–rezoluciju. Ponovno napomenimo da SLD–rezolucija nije potpuna na skupu svih formula logike prvog reda, nego samo na skupu Hornovih klauzula, odnosno programu. Dokazi teorema mogu se pronaći, primjerice, u [3].

Primijetimo da teorem potpunosti kaže da postoji neki izvod prazne klauzule neovisno o korištenom pravilu izračunavanja. Pravilo pretraživanja, s druge strane, određuje hoće li se izvod pronaći i koliko efikasno će pretraživanje biti. Ova pravila su važna jer definiraju proceduralni aspekt logičkog programa. Posljedica toga je da možemo imati logičke programe koji imaju istu semantičku, ali različite proceduralne interpretacije. To znači da izvod prazne klauzule može postojati, ali da SLD–rezolucija nikada ne stane s radom!

Postoji suptilna razlika između notacije koja se koristi u Prologu i notacije koju koristimo u logici prvog reda. Simbol „ \leftarrow" za kondicional zamjenjujemo simbolom „ :-", dok umjesto simbola „\wedge" za konjunkciju koristimo zarez. Individualne varijable pišemo velikim početnim slovom ili simbolom „ _", dok relacijske, funkcijske i konstantske simbole označavamo proizvoljnim riječima koje počinju malim početnim slovom. Negaciju označavamo simbolom „ \+". U Prologu je pravilo pretraživanja definirano tako da se potraga za programskom klauzulom (procedurom) provodi od početka (vrha) programa prema kraju (dnu) programa, dok je pravilo izračunavanja definirano tako da se za podudaranje odabire prvi literal s lijeva u ciljnoj klauzuli. Dakle, za pravilo izračunavanja Prolog koristi depth-first search (DFS) algoritam.

Sada nam je cilj na nekoliko jednostavnih primjera povezati teoriju s programima pisanim u Prologu. Primjeri koji slijede pisani su u GNU Prolog implementaciji koja se može preuzeti na adresi: http://www.gprolog.org .

Prvo dajemo jedan vrlo jednostavan primjer kojim želimo opisati utjecanje nekih rijeka u more. Njime želimo istaknuti osnovnu sintaksu Prologa, kao i način na koji Prolog interpreter (koji implementira rezoluciju) dolazi do zaljučaka.

utječeU(drava, sava).
utječeU(sava, dunav).
utječeU(dunav, 'crno more').

more('crno more').

uMore(C, D) :- utječeU(C, D), more(D).
uMore(C, M) :- utječeU(C, D), uMore(D, M).

Ovo je primjer jednog logičkog programa koji se sastoji od tri procedure, od kojih su procedure s relacijskim simbolima „ utječeU" i „ more" ujedno i baze znanja (sastoje se od činjenica koje ne sadrže individualne varijable). Ovaj vrlo jednostavan primjer iz osnovnih upita oblika „ kamo utječe neka rijeka" izvodi zaključke oblika „ voda neke rijeke završava u nekom moru", ako se „ more" definira kao „ ono što nikamo ne utječe". Činjenicu da rijeka Drava utječe u rijeku Savu u Prologu iskazujemo kao „ utječeU(drava, sava)". Također, činjenicu da je Crno more neko more, u Prologu iskazujemo kao „ more('crno more')". S druge strane, da bismo opisali da neka rijeka utječe u Crno more, ona mora ili utjecati u njega, što iskazujemo pomoću procedure „ uMore(C, D) :- utječeU(C, D), more(D)", ili utjecati u neku rijeku koja dalje utječe u Crno more, što iskazujemo pomoću rekurzivne procedure „ uMore(C, M) :- utječeU(C, D), uMore(D, M)". Efektivno, ovo je način na koji se može modelirati tranzitivno zatvorenje neke relacije.

Da bismo dokazali da Dunav utječe u Crno more, Prologu postavljamo upit pomoću ciljne klauzule G_{0}\equiv\texttt{:- uMore(dunav, 'crno more')}. Nakon toga, Prolog pretražuje program od vrha prema dnu (prema pravilu pretraživanja) pokušavajući pritom pronaći programsku klauzulu čiju glavu može unificirati s prvim lijevim literalom u ciljnoj klauzuli G_{0} (prema pravilu izračunavanja), što je literal A_{0}\equiv\texttt{uMore(dunav, 'crno more')}. Tražena klauzula je C_{0}\equiv\texttt{uMore(C, D) :- utječeU(C, D), more(D)}, čiju glavu ćemo označiti s B_{0}. Dakle, iz unifikacije A_{0}\theta_{0}\equiv B_{0}\theta_{0} dobivamo unifikator \theta=\lbrace C\leftarrow\texttt{dunav},D\leftarrow\texttt{'crno more'}\rbrace i novu ciljnu klauzulu G_{1}\equiv\texttt{:- utječeU(dunav, 'crno more'), more('crno more')}. Sada istim postupkom ponovno tražimo programsku klauzulu čiju glavu možemo unificirati s prvim lijevim literalom u G_{1} i tako dobivamo ciljnu klauzulu G_{2}\equiv\texttt{:- more('crno more')}. Budući da nam je ostao jedan literal u ciljnoj klauzuli G_{2}, kojeg možemo unificirati s glavom jedne od programskih klauzula, za rezultat dobivamo praznu klauzulu, odnosno G_{3}\equiv\square. Time smo dobili SLD–izvod prazne klauzule i dokazali da rijeka Dunav utječe u Crno more.

| ?- uMore(dunav, 'crno more').
true ?
yes

Prologov odgovor “true” jest jedna (prazna) unifikacija koja čini ovu klauzulu istinitom. Upitnik znači da je Prolog stao čim je našao jedno rješenje, te nas pita za dalji postupak. Ako samo pritisnemo Enter, dobijemo odgovor “yes” kao gore. Ako pritisnemo tipku `;' (sljedeće rješenje) ili `a' (sva rješenja), dobijemo odgovor “no”, što znači da nema više rješenja.

Pretpostavimo sada da želimo doznati koja rijeka utječe u Crno more. Taj upit izražavamo pomoću ciljne klauzule G\equiv\texttt{:- uMore(X, 'crno more')}, gdje je X sada individualna varijabla.

Rad Prologa prikazujemo sljedećim koracima. Prvi lijevi literal u ciljnoj klauzuli nećemo posebno naglašavati.

G_{0} \equiv \texttt{:- uMore(X, 'crno more')};
C_{0} \equiv \texttt{uMore(C, D) :- utječeU(C, D), more(D)},
\theta_{0}=\lbrace \texttt{C}\leftarrow\texttt{X},\texttt{D}\leftarrow \texttt{'crno more'}\rbrace ;
G_{1} \equiv \texttt{:- utječeU(X, 'crno more'), more('crno more')};
C_{1} \equiv \texttt{utječeU(dunav, 'crno more')},
\theta_{1}=\lbrace \texttt{X}\leftarrow\texttt{dunav}\rbrace ;
G_{2} \equiv \texttt{:- more('crno more')};
C_{2} \equiv \texttt{more('crno more')};
\theta_{2} = \epsilon;
G_{3}\equiv\square;

Iz teorema adekvatnosti slijedi da je supstitucija \theta = \theta_{0}\theta_{1}\theta_{2}\restriction_{\verb+X+} (gdje s \restriction_{\verb+X+} označavamo restrikciju na individualnu varijablu \verb+X+) supstitucija korektnog odgovora i vrijedi P\Rightarrow \lnot G\theta, odnosno P\Rightarrow\texttt{uMore(dunav, 'crno more')}, gdje je P oznaka za naš program. Prolog bi nam, za ovaj upit, uzvratio odgovorom „\verb+X = dunav+". Međutim, ovo očito nije jedino rješenje. U slučaju da želimo još jedno rješenje, Prolog se tada mora vratiti do trenutka kada je mogao drukčije supstituirati individualnu varijablu X. To je očito trenutak prije odabira klauzule C_{0}. Promotrimo rad Prologa u tom slučaju.

G_{0} \equiv \texttt{:- uMore(X, 'crno more')};
C_{0} \equiv \texttt{uMore(C, M) :- utječeU(C, D), uMore(D, M)},
\theta_{0}=\lbrace \texttt{C}\leftarrow\texttt{X},\texttt{M}\leftarrow \texttt{'crno more'}\rbrace ;
G_{1} \equiv \texttt{:- utječeU(X, D), uMore(D, 'crno more')};
C_{1} \equiv \texttt{utječeU(drava, sava)},
\theta_{1}=\lbrace \texttt{X}\leftarrow\texttt{drava},\texttt{D}\leftarrow \texttt{sava}\rbrace ;
G_{2} \equiv \texttt{:- uMore(sava, 'crno more')};
C_{2}' \equiv \texttt{uMore(C, D) :- utječeU(C, D), more(D)},
\theta_{2}'=\lbrace \texttt{C}\leftarrow\texttt{sava},\texttt{D}\leftarrow \texttt{'crno more'}\rbrace ;
G_{3}' \equiv \texttt{:- utječeU(sava, 'crno more'), more('crno more')};

Budući da rijeka Sava ne utječe direktno u Crno more, Prolog pomoću ciljne klauzule G_{3}' ne može generirati praznu klauzulu. U tom slučaju, Prolog se vraća do zadnjeg trenutka kad je mogao odabrati drugu programsku klauzulu. To je trenutak prije odabira klauzule C_{2}.

C_{2} \equiv \texttt{uMore(C, M) :- utječeU(C, D), uMore(D, M)},
\theta_{2}=\lbrace \texttt{C}\leftarrow\texttt{sava},\texttt{M}\leftarrow \texttt{'crno more'}\rbrace ;
G_{3} \equiv \texttt{:- utječeU(sava, D), uMore(D, 'crno more')};
C_{3} \equiv \texttt{utječeU(sava, dunav)},
\theta_{3}=\lbrace \texttt{D}\leftarrow\texttt{sava}\rbrace ;
G_{4} \equiv \texttt{:- uMore(dunav, 'crno more')};
C_{4} \equiv \texttt{uMore(C, D) :- utječeU(C, D), more(D)},
\theta_{4}=\lbrace \texttt{C}\leftarrow\texttt{dunav},\texttt{D}\leftarrow \texttt{'crno more'}\rbrace ;
G_{5} \equiv \texttt{:- utječeU(dunav, 'crno more'), more('crno more')};
C_{5} \equiv \texttt{utječeU(dunav, 'crno more')},
\theta_{5}=\epsilon;
G_{6} \equiv \texttt{:- more('crno more')};
C_{6} \equiv \texttt{more('crno more')};
\theta_{6} = \epsilon;
G_{7}\equiv\square;

Iz teorema adekvatnosti slijedi da je supstitucija \theta = \theta_{0}\theta_{1}\theta_{2}\theta_{3} \theta_{4}\theta_{5}\theta_{6}\restriction_{\verb+X+} supstitucija korektnog odgovora i vrijedi P\Rightarrow\texttt{uMore(drava, 'crno more')}. Prolog bi nam sada uzvratio odgovorom „\verb+X = drava+". Sada bismo na isti način mogli dobiti i P\Rightarrow\texttt{uMore(sava, 'crno more')}, no primijetimo da bi u tom slučaju Prolog nekoliko puta skrenuo u „ slijepu ulicu", sve dok se ne bi vratio do trenutka prije odabira klauzule C_{1}.

| ?- uMore(X, 'crno more').
X = dunav ? a
X = drava
X = sava
no

Još smo prije naglasili da možemo imati programe koji imaju istu semantičku, no različite proceduralne interpretacije. Ako u zadnjoj programskoj klauzuli zamijenimo poredak literala, te nakon toga zamijenimo poredak zadnje dvije programske klauzule, dobit ćemo program koji očito ima isto semantičko značenje (jer su konjunkcija i disjunkcija semantički komutativne), no Prolog neće stati s radom prilikom upita „uMore(drava, 'crno more')".

Drugi primjer (traženje telefona u kompliciranoj kući s puno soba) pokazuje kako primjenom listi možemo pamtiti proizvoljno komplicirane strukture tijekom traženja. Liste su samo sintaktički istaknute strukture dobivene uzastopnom primjenom binarnog predikata ., koji veže početni element i ostatak liste: svaka lista je ili [] (prazna), ili oblika [H|T]\equiv.(H,T), gdje je H početni element, a T lista preostalih elemenata. Kako je graf ovdje po prirodi neusmjeren (vrata funkcioniraju u oba smjera), za izbjegavanje beskonačnih petlji moramo voditi evidenciju o tome kroz koje sobe smo već prošli, kako ih ne bismo ponavljali u obilasku.

 
door(a, b). % +--------------+
door(b, e). % |  d      c    |
door(b, c). % +----  ----  --+
door(d, e). % | f   e     b     a
door(c, d). % +------  +-----+
door(e, f). % |    g   |
door(g, e). % +--------+

hasPhone(g).
go(X, X, _, []).
go(X, Y, T, [Z|Result]):-
    (door(X, Z); door(Z, X)),
    \+ member(Z,T),
    go(Z, Y, [Z|T], Result).
findphone(Path) :-
    go(a, Target, [], Path),
    hasPhone(Target).

Predikat go(From, To, Avoid, Result) izražava činjenicu da je lista Result jedna moguća staza od sobe From do sobe To, izbjegavajući sobe na listi Avoid. Znak ; u klauzuli (door(X, Z); door(Z, X)) označava logičku disjunkciju: Prolog će pokušati zadovoljiti prvi disjunkt, a nakon backtrackinga (vraćanja na istu točku u DFS obilasku) će pokušati zadovoljiti drugi. To je jednostavan način da zapišemo simetrične relacije: tako možemo u bazi znanja popisati samo veze u jednom smjeru, a u logici programa reći da ih je moguće prelaziti u oba smjera.

Pozivom predikata findphone kažemo Prologu da pronađe stazu kojom se moramo kretati da bismo kroz kuću došli do neke sobe s telefonom (u primjeru je to jedino soba g). Kao što vidimo, lista “zabranjenih” soba nam omogućuje da tražimo samo jednostavne staze (koje ne ponavljaju sobe), kojih ima konačno mnogo, pa ih Prolog može sve pronaći čak i DFS obilaskom.

| ?- findphone(Path).
Path = [b,e,g] ? a
Path = [b,c,d,e,g]
no

Pored direktnog zaključivanja pomoću Hornovih klauzula, Prolog omogućuje i redukciju bilo kakvih uvjeta nad konačnim domenama (s propagacijom ograničenja), što bitno pojednostavljuje programiranje u mnogim slučajevima.

U nekim implementacijama Prologa ta funkcionalnost nalazi se u biblioteci clpfd (Constraint Logic Programming over Finite Domains), no GNU Prolog je uključuje u osnovni jezik.

Zadatak. Treba pronaći sve načine na koje 500\, \text{k}g brašna možemo rasporediti u vreće od 40\, \text{k}g i 60\, \text{k}g. Primijetimo da je dovoljno zadati uvjete nenegativnosti varijabli: Prolog tada iz jednadžbe zaključuje gornje ograde na njih, iz čega odmah dobiva informaciju da su nad konačnim domenama (implicitna je pretpostavka da su cijeli brojevi). Tada se propagacijom uvjeta lako dobivaju sve mogućnosti.

vreće(V40, V60) :-
    V40 #>= 0, V60 #>= 0,
    V40 * 40 + V60 * 60 #= 500,
    fd_labeling([V40, V60]).

Programiranje je vrlo slično uobičajenom logičkom programiranju u Prologu: popišemo uvjete (svi operatori biblioteke clpfd pišu se s početnim znakom # da bi se razlikovali od ugrađenih Prologovih operatora), i pomoću fd_labeling([varijable]) zatražimo rješenja.

| ?- vreće(Male, Velike).

Male = 2
Velike = 7 ? a

Male = 5
Velike = 5

Male = 8
Velike = 3

Male = 11
Velike = 1

yes

Važno je napomenuti da su parcijalne interpretacije u logici sudova, definirane samo na varijablama koje se pojavljuju u nekom konačnom skupu formula, samo specijalni slučaj varijable nad konačnom domenom (2^{n} mogućnosti, gdje je n ukupni broj varijabli). To znači da primjenom upravo opisane tehnike možemo rješavati i zadatke sljedećeg tipa.

Zadatak.2 Gazdarica na zabavi reče da će besplatni šampanjac dobiti onaj tko ispuni sljedeće uvjete:

}

Rješenje zadatka je dano sljedećim Prolog programom. Primijetimo da se pojavljuje logički veznik „osim ako” kojeg Prolog nema definiranog, ali ga možemo lako definirati pomoću implikacije. Deklariranju takvih operatora služi op naredba: 740 je razina prioriteta (ista kao za #==>), a xfx znači da želimo binarni neasocijativni operator.

:- op(740, xfx, osimako).
A osimako B :- #\ B #==> A.

šampanjac :-
    #\ K #\/ C #==> #\ G #/\ P,
    G #/\ #\ K osimako C #/\ #\ P,
    fd_labeling([G, K, C, P]).

Nakon unošenja prethodnog programa, na upit ?- šampanjac., Prolog daje odgovor “no” (ili “false.”, ovisno o implementaciji). To znači da gazdaričine uvjete nije moguće ispuniti.

Na kraju navodimo kratak pregled povijesti logičkog programiranja. Više detalja možete pročitati u [7].

Iako se ideje o logičkom programiranju mogu pronaći još u intuicionističkoj logici i teoriji dokaza s početka dvadesetog stoljeća, možemo reći da je logičko programiranje kakvog danas poznajemo direktna posljedica ranijeg razvoja automatiziranih dokazivača teorema i umjetne inteligencije iz šezdesetih godina dvadesetog stoljeća. Značajan trenutak u tom razvoju bio je uvođenje metode opće rezolucije (1965) od strane Johna Alana Robinsona. Iako je pravilo rezolucije bilo poznato još prije kod primjene u logici sudova (na primjer kod Davis–Putnamova algoritma), Robinson ga je u svom radu uspio ujediniti s metodom unifikacije, te dokazati adekvatnost i potpunost tako dobivene metode opće rezolucije. Ovaj rezultat je pokrenuo novi val istraživanja automatiziranih dokazivača teorema i mnogi znanstvenici su se okrenuli proučavanju raznih restrikcija pravila opće rezolucije.

Robert Kowalski je 1972. godine došao na ideju da SL–rezoluciju primijeni na Hornovim klauzulama. Takva rezolucija je poslije dobila ime SLD–rezolucija. Na temelju njegovog rada, Alan Colmerauer i Philippe Roussel dizajniraju efikasan logički programski jezik u svrhu procesiranja prirodnog jezika kojeg Roussel naziva Prolog (Programmation Logique). Prvi Prolog interpreter napisao je Roussel u programskom jeziku ALGOL–W, dok se nedugo zatim pojavila poboljšana verzija napisana u programskom jeziku FORTRAN. Prolog je bio dokaz da programski jezik može imati dualnu interpretaciju — deklarativnu od strane programera i proceduralnu od strane parsera.

Velik korak u razvoju Prologa nastao je pojavom Warrenove apstraktne mašine (WAM). Istu je dizajnirao David Warren u svrhu efikasnijeg izvršavanja Prolog programa. WAM je danas postao meta skoro svih Prolog prevoditelja. Na razvoj Prologa također je utjecao i FGCS (eng. Fifth Generation Computer Systems Project). Paralelizirana varijanta Prologa pod imenom KL1 (eng. Kernel Language 1) korištena je kao jezik operativnog sustava za FGCS.

Prolog je danas daleko najpopularniji logički (odnosno deklarativni) programski jezik. Postoje mnoge kvalitetne Prolog implementacije. Neke od njih su GNU Prolog, SWI–Prolog, Visual Prolog i YAP–Prolog. Prolog je, također, utjecao na pojavu novih programskih jezika. Neki od značajnijih su DATALOG, Mercury, Gödel i Erlang.