Ugrás a tartalomhoz

A matematikai logika alkalmazásszemléletű tárgyalása

Pásztorné Varga Katalin, Várterész Magda, Sági Gábor

Panem Kft.

A logikai programozásról

A logikai programozásról

Ismertettünk az automatikus tételbizonyításra néhány kalkulust: a bizonyításelméleti kalkulust (Hilbert-rendszer), a szekventkalkulusokat, a rezolúciós kalkulusokat és a tablók módszerét. Ha egy problémát sikerül megfogalmazni mint feltételformulák és speciális axiómaformulák lehetséges következményét, azaz sikerül a problémát tételbizonyítási feladattá alakítani, akkor az ismert tételbizonyító kalkulusok bármelyikével megkísérelhető a feladat megoldása. Amennyiben egy tételbizonyító kalkulus számítógépes implementációja adott, akkor ez a megadott formulák alapján megpróbálja eldönteni, hogy a tételbizonyítási feladatra mi a válasz. Ennek megfelelően logikai programozási nyelvnek tekinthetünk minden elsőrendű logikai nyelvet. Kétféle módon szokás a tételbizonyítási feladatot leíró formulák együttesét minősíteni. Ha az implementált kalkulust mint számítógépes programot tekintjük, akkor a kalkulust megvalósító programnak a szóban forgó formulák ,,adatai”. Ebben az esetben a logikai nyelv adatdefiniáló, adatleíró nyelvnek minősül. Ha az implementált kalkulust mint speciális számítógépet tekintjük, akkor a logikai nyelven leírt formulák e ,,logikai gép programjai”. Ebben az esetben a logikai nyelv egy programnyelv. Ezek a gondolatok az 1970-es évek kutatásaiban jelennek meg ([37]), és ez az az időszak, amikor a lineáris inputstratégiát alkalmazó rezolúciós kalkulus egy változatát számítógépen megvalósítják. Az implementált kalkulushoz a programozási nyelv a Prolog[12] ([36,39]). Az első Prolog interpreter Marseille-ben 1972-ben Colmerauer, és röviddel utána Magyarországon Szeredi Péter nevéhez fűződik. Ezeket számos helyen követték újabb interpreterek és később fordítóprogramok. A Prologhoz készült fordítók eljárásorientált értelmezését adták a nyelvnek. A Prologot a számítástudományban mint specifikációs és mint deklaratív nyelvet is használják. Az újabb logikai programozási rendszerek az 1980-as évekre jelentek meg ([10,62]). Ugyanígy erre az időre tehető a logikai programozás lehetőségeit és korlátait kutató munkák eredményeinek összegzése ([4,39]). Az utóbbi évek összefoglaló műveiből ([5,46,47,67]) képet kaphatunk a fejlődés irányáról és az újabb elképzelésekről.

A Prolog nyelv

Legyen egy tételbizonyítási feladat a feltételformuláknak és a tétel negáltjának Skolem-normálformáiból előálló elsőrendű klózok F1,F2,,Fk,¬T alakú sorozatával megadva. Egy zárt Skolem-normálforma logikailag ekvivalens a mag klózaiból alkotott elsőrendű klózok konjunkciójával:

x 1 x s ( K 1 K l ) x 1 x s K 1 x 1 x s K l .

Egy elsőrendű klóz általános alakja

x 1 x s ( A 1 A n ¬ B 1 ¬ B m ) ,

ahol Ai és Bj különböző atomi formulák. Az elsőrendű klózt szokták

A 1 , , A n : B 1 , , B m

alakban is írni. A kvantorokat ugyanis nem érdemes feltüntetni, hiszen tudjuk, hogy minden individuumváltozó szerint univerzálisan kvantálunk. A negáció jelet sem kell odaírni a B1,,Bm formulák elé, mert ezek az atomok mind a :- jel jobb oldalán állnak, és innen tudni fogjuk, hogy negáltak. A diszjunkció jele helyett pedig egyszerűen vesszőt írunk. A fenti általános elsőrendű klóz logikailag ekvivalens a

x 1 x s ( B 1 B m A 1 A n )

formulával. Emiatt :- jel bal oldalán álló A1,,An literálok az ún. diszjunktív vagy alternatív feltételek. Ezt a részt a klóz fejének (head) nevezzük. A :- jel jobb oldalán álló B1,,Bm literálok a konjunktív vagy összetartozó feltételek. Ezt a részt pedig a klóz törzsének (body) nevezzük.

Egy Prolog program ,,utasításai” olyan elsőrendű klózok, melyek feje egyetlen literál, vagyis a logikai program klózai A:B1,,Bm vagy A alakú klózok lehetnek. Ezeket a klózokat definit programklózoknak nevezzük utalva arra, hogy egy ilyen klóz úgy is tekinthető, mint a klózbeli (egyetlen) pozitív literál definíciója. Szokás az A:B1,,Bm alakú definit klózokat szabályoknak, az A alakúakat pedig tényeknek is nevezni.

7.2.1. DEFINÍCIÓ. Definit programklózok véges sorozatát definit programnak nevezzük. Egy definit programban azon klózok halmaza, amelyeknek a feje ugyanazon predikátumszimbólummal kezdődő atomi formula, a predikátum definíciója. A definícióban szereplő klózok egy sorozata pedig a definit program partíciója.

A Prolog programban egy predikátum definíciójában szereplő összes klózt egymásután, egy partícióban kell feltüntetni. A partícióban a programklózok sorrendjét és persze a törzsben a literálok sorrendjét is a programozó határozza meg a megfelelő sorrendbe írással. Ezen a sorrenden a Prolog fordító nem változtat.

A Prolog programhoz tartozik a tételformula negáltjából kapott klóz is, amelyet definit célklóznak nevezünk és csak negált literálokat tartalmazhat. Tehát mint formula a célklóz

x 1 x s ( ¬ C 1 ¬ C n )

alakú (ahol Ci atom), ami a programban :C1,,Cn formában írunk le. Ez azt mutatja, hogy egy Prolog program (alapesetben) csak

x 1 x s ( C 1 C n )

alakú tételformulákat tud kezelni. A Prolog programozási nyelvben tehát definit programklózokkal és definit célklózzal, azaz Horn-klózokkal dolgozunk.

A Prolog program olyan definit program, melyet egy definit célklóz megadása után az SLD[13] algoritmus kezel. Az SLD betűszó arra utal, hogy az algoritmus

(D) definit programklózokat használ,

(L) lineáris inputstratégiával dolgozik,

(S) a célklózban a feldolgozandó literált és e literálnak megfelelő partícióból a rezolválás során felhasználandó programklózt egy rögzített (S) stratégia alapján választja ki.

Az SLD algoritmus az illesztő helyettesítést és a faktorizálást az elsőrendű rezolúciós kalkulusnál definiált módon alkalmazza. A rezolvensképzés folyamata a következő: ha

: C 1 , , C n

a célklóz, az (S) stratégia szerint Ci(1in) a belőle kiválasztott literál és

A : B 1 , , B m

a literálnak megfelelő partícióból kiválasztott programklóz, továbbá ha A és Ci illeszthető valamely θ illesztő helyettesítéssel, akkor a rezolvens a következő:

: C 1 θ , , C i 1 θ , B 1 θ , , B m θ , C i + 1 θ , , C n θ .

Az algoritmus a célklózból indul és a programklózok szerkezete miatt minden rezolvens is célklóz alakú lesz.

Az SLD algoritmus a teljes levezetési fát a ,,mélységben először” bejárási módnak megfelelően építi:

  1. Legyen az aktuális célklóz az eredeti célklóz, azaz a levezetési fa gyökere.

  2. Ha az aktuális célklóz az üres klóz, akkor megkaptunk egy rezolúciós cáfolatot. A célklóz ,,sikeres” minősítést kap: az algoritmus jelzi, hogy van sikeres levezetés, majd a levezetési fa építésében a 6. lépés következik. Ha pedig az aktuális célklóz nem az üres klóz, akkor a 3. lépéssel folytatjuk a levezetési fa építését.

  3. Kiválasztjuk az aktuális célklózból a ,,balról első” literált (azaz az (S) stratégia szerint választunk).

  4. Kiválasztjuk hozzá a megfelelő fejjel rendelkező partícióból a soron következő (induláskor az első) programklózt (szintén az (S) stratégia szerint választunk). Ha a partíciónak nincs (már több) eleme, akkor a 6. pont következik.

  5. Ha a kiválasztott célklózbeli literál és a programklóz fejének az illesztése sikeres, akkor előállítjuk a rezolvenst, ez lesz az új aktuális célklóz és az 2. pont következik. Egyébként ez a választás ,,kudarcos” minősítést kap, és újból a 4. pont következik.

  6. Ha az aktuális célklóz a gyökér, az algoritmus befejeződik. Egyébként visszalépünk az aktuális célklózból az előző célklózra, ez lesz az új aktuális célklóz, és a 3. lépéssel folytatjuk a levezetési fa építését.

Használhatunk olyan (S) stratégiát is, amely mindig a célklóz ,,jobbról első” literálját választja ki. Azonban ez a két kiválasztási stratégia merev, emiatt a lineáris inputrezolúció nem teljes Horn-klózhalmazokra sem.

7.2.2. MEGJEGYZÉS. A továbbiakban a Prolog programokat az [62]-ban bevezetett és széles körben használt szintaxis szerint írjuk: a predikátum- és konstansszimbólumokat kisbetűvel, az individuumváltozókat nagybetűvel kezdődő karaktersorozattal jelöljük.

7.2.3. PÉLDA. Vizsgáljuk meg a következő Prolog programot:

programklózok

p(X,Z) :-q(X,Y), p(Y,Z).

p(X,X).

q(a,b).

célklóz

:- p(X,b).

Az első két programklóz feje ugyanazt a predikátumszimbólumot tartalmazza, így ezek egy partíciót alkotnak.

  1. A 7.1. ábra azt mutatja, hogy a ,,balról első” célklózbeli literál kiválasztási stratégia mellett az SLD algoritmus megtalálja mindkét sikeres levezetést.

Figure 7.1. Véges SLD fa

Véges SLD fa

  1. A 7.2. ábra pedig azt mutatja, hogy a ,,jobbról első” célklózbeli literál kiválasztási stratégia mellett az SLD algoritmus nem képes bejárni a teljes levezetési fát, mivel mindig a legbaloldalibb ágon marad.

Figure 7.2. Végtelen SLD fa

Végtelen SLD fa

7.2.4. MEGJEGYZÉS. A stratégia ismeretében a program írása során a literálok és a partíciók klózainak sorrendjére ügyelve a fenti példában jelzett probléma elkerülhető. Az (S) stratégia javítása miatt az újabb Prolog fordítókban a probléma már elő sem fordul.

Mivel a lineáris inputrezolúciós stratégiával az algoritmus bejárja a teljes levezetési fát, ami sok esetben gazdaságtalanná teszi a Prolog program ,,futását”, ezért bevezettek néhány eszközt a vezérlés hatékonyabbá tételére. Ezeket az eszközöket a programozó írja be a programba a feladat ismeretében. Az egyik ilyen eszköz a fail ,,predikátum”, amely mindig kudarc állapotot jelez, és ezzel visszalépésre készteti az algoritmust. A másik ilyen eszköz a vágás vagy cut (!) ,,predikátum”, amely – mint mindig sikeresen rezolválható literál – nem a rezolúciós algoritmus előrehaladását befolyásolja, hanem a visszalépés során fejti ki hatását az algoritmus vezérlésére. Mielőtt megadnánk ezen eszközök pontos hatását, vezessük be a következő fogalmat:

7.2.5. DEFINÍCIÓ. Egy lineáris inputrezolúciós levezetésben egy centrális klózbeli L literál közvetlen őse az a centrális klózbeli literál, amelyet az L literált tartalmazó mellékklóz fejével rezolváltunk. Lőse pedig a közvetlen őse, valamint ha egy literál L őse, akkor annak közvetlen őse is.

Az SLD algoritmus és a külön bevezetett segédeszközök működésének illusztrációja során az alábbi példákban logikai programok sémáival dolgozunk, azaz a programklózokban és a célklózban a literálokat szimbólumokkal helyettesítjük.

7.2.6. PÉLDA. Őskeresés egy levezetésben.

program

A :- B, C.

levezetés

:- A. *

B :- E.

A :- B, C.

C :- D, E, F.

:- B, C.

C :- A.

B :- E.

D.

:- E, C.

E.

E.

cél

:- A.

:- C. *

C :- D, E, F.

:- D, E, F.

D.

:- E, F.

E.

:- F.

A *-gal jelölt literálok a levezetésben szereplő :- F centrális klóz ősei.

Most adjuk meg a vágás (!) predikátum hatását. Ha a visszalépés során egy vágást, azaz !-t mint feldolgozott célliterált érint az algoritmus, akkor annak közvetlen ősét kudarcosnak tekinti, még egy szintet visszalép, és onnan folytatja a levezetési fa bejárását. A ! alkalmazásával az algoritmus vezérlése úgy módosul, hogy a teljes levezetési fa bizonyos részfáit be sem járja az algoritmus.

7.2.7. PÉLDA. Bővítsük a fenti feladatot egy vágás bevezetésével, és vizsgájuk meg annak hatását.

program

A :- B, C.

levezetés

:- A.

B :- E.

A :- B, C.

C :- D, E, !, F.

:- B, C.

C :- A.

B :- E.

D.

:- E, C.

E.

E.

cél

:- A.

:- C. *

C :- D, E, !, F.

:- D, E, !, F.

D.

:- E, !, F.

E.

:- !, F.

!.

kudarc

:- F.

A visszalépés során az algoritmus érinti a :- !, F literált. Ennek közvetlen őse a -gal jelölt :- C. A C partíció kételemű, de a vágás miatt :- C-t érintve az algoritmus nem vizsgálja a partíció másik programklózát, hanem még egy szintet visszalép :- E, C-re. Jelen példában innen megint visszalépünk a :- B, C, végül az :- A klózokra, és a program kudarccal fejeződik be.

Most két olyan feladatot mutatunk, amelyeket vágás nélkül nem lehetne SLD rezolúcióval megoldani.

  1. Az IF F THEN V1 ELSE V2 programkonstrukcióra a Prolog fordítóprogramok általában tartalmaznak beépített eljárást. Ez a konstrukció két logikai program – p1 és p2 – összekapcsolásával állít elő egy olyan logikai programot, ahol az F feltételformula igazságértékétől függően vagy V1, azaz a p1 program végrehajtása, vagy V2, azaz a p2 program végrehajtása következik be.

program

if(F,V1,V2) :- F, !, V1.

if(F,V1,V2) :- V2.

Legyen f a feltételt leíró logikai program, a és b pedig rendre a p1 és p2 logikai programokat aktivizáló célklózok. Ekkor az :- if(f,a,b) cél esetén ha az f feltétel nem igaz, akkor az algoritmus visszalép, és a partíció második elemét dolgozza fel, aminek b feldolgozása az eredménye. Ha az f feltétel igaz, akkor a ! után az a kerül feldolgozásra. Ha a futása kudarcos lenne, akkor az algoritmus visszalépne, érintené a !-t, és az őst (:- if(f,a,b)) kudarcosnak minősítené.

  1. A negáció értelmezése. A szokásos negáció az SLD algoritmussal nem kezelhető, hiszen :- ¬ C alakú célklóz nem megengedett. Bevezetjük a not C alakú ,,literált”, és az alábbi logikai programmal definiáljuk a negációt. Azaz ha C-vel nem vezethető le az üres klóz, akkor ¬ C igaz.

program

not X :- X, !, fail.

not X.

cél

:- not C.

X itt egy literállal illeszthető változót jelent. A partíció első klózával indít az algoritmus. Ha C levezetése sikeres, akkor az algoritmus átlép a !-n, és a fail miatt visszalép. A ! közvetlen őse a :- not C, ami a gyökér, így az algoritmus eredménye kudarcos. Ha pedig a C partíciójának klózai nem illeszthetők C-vel vagy nincs C-re partíció, akkor az algoritmus visszalép, és a partíció második klóza miatt sikeres. A C literál ,,negáltja” tehát a program következménye. Ezt a negációt a logikai programozásban ,,negáció mint kudarc”-nak nevezik.

Vegyük észre, hogy ha a partícióban a klózok sorrendjét felcseréljük, a kapott program nem lesz alkalmas a negáció értelmezésére:

program

not X.

not X :- X, !, fail.

cél

:- not C.

A partíció első klózával indít az algoritmus. Ez a :- not C-vel mindig illeszthető. Az eredmény az, hogy bármely C literál ,,negáltja” következmény, ami nyilvánvalóan nem jó megoldás.

7.2.8. DEFINÍCIÓ. Legyen P egy definit program és G egy definit célklóz. Legyen továbbá θ a G-ben előforduló individuumváltozóknak tetszőleges termhelyettesítése. θ-t P{G}-re vonatkozó válaszhelyettesítésnek, röviden válasznak nevezzük. Legyen θ egy P{:C1,,Cn}-re vonatkozó válasz. Azt mondjuk, hogy θkorrekt válasz, ha a

x 1 x s ( C 1 θ C n θ )

formula logikai következménye P-nek, ahol x1,,xs a C1θCnθ formula szabad változói.

Tehát θ korrekt válasz P{:C1,,Cn}-re, ha C1θCnθ minden Herbrand-univerzum feletti alappéldánya logikai következménye P-nek. Azt a választ, amely a rezolúciós levezetés során áll elő G individuumváltozóira, kiszámított válasznak nevezzük. Nyilvánvaló, hogy a rezolúciós cáfolat során kiszámított válasz korrekt. A 7.2.3. példában szereplő klózhalmaz Herbrand-univerzuma {a,b}. A 7.1. ábrán látható két sikeres rezolúciós cáfolat pedig az (Xa), illetve az (Xb) alaphelyettesítéssel mint válasszal állt elő.

A Prolog programban megengedett az ún. rekurzív programklóz használata. Ennek általános alakja egy

p(U,V).

p(X,Y) :- q(Y1), p(X1,Y1).

alakú partíció. Ez mutatja, hogy p definíciója függ annak egy példányától, és az elvárt eredmény alakja p(U,V) (megállási feltétel). Ez a lehetőség olyan feladatok kezelésére is alkalmas, amelyeket elsőrendű nyelven nem lehetne leírni. Sőt így lehetővé válik rekurzív függvényekkel megfogalmazható problémák kezelése is. Lássunk – a teljesség igénye nélkül – néhány ilyen problémát.

  1. Családi kapcsolatok leírása során a szülője, nagyszülője, anyja, apja, gyermeke kapcsolatok leírhatók elsőrendű formulával:

x y ( A p j a ( x , y ) A n y j a ( x , y ) S z ü l ő j e ( x , y ) )

x y z ( A p j a ( x , y ) S z ü l ő j e ( y , z ) N a g y a p j a ( x , z ) )

x y z ( A n y j a ( x , y ) S z ü l ő j e ( y , z ) N a g y a n y j a ( x , z ) )

A megfelelő Prolog program:

szülője(X,Y) :- apja(X,Y).

szülője(X,Y) :- anyja(X,Y).

nagyapja(X,Z) :- apja(X,Y), szülője(Y,Z).

nagyanyja(X,Z) :- anyja(X,Y), szülője(Y,Z).

Az őse kapcsolat azonban csak rekurzióval adható meg, hiszen egy ember ősei nem csak az anyja és az apja, hanem szüleinek ősei is. Az őse kapcsolat leírása Prolog programklózokkal:

őse(X,Y) :- szülője(X,Y).

őse(X,Y) :- szülője(X,Z), őse(Z,Y).

  1. Definiáljuk Prologban az utat a gráfban. Bevezetjük az él(X,Y) predikátumot annak jelölésére, hogyX-ből Y-ba vezet él. Ezek után az út definícióját megadó Prolog program:

út(X,Y) :- él(X,Y).

út(X,Y) :- él(X,Z), út(Z,Y).

A Prologban fontos szerepet játszik, hogy termeknek véges sorozataival, az ún. listákkal is tudunk dolgozni. A lista jelölése: [t1,t2,…,tn], ahol t1,t2,…,tn a lista elemei. A t1 elemet a lista fejének, a [t2,…,tn] listát pedig a lista toldalékának nevezzük. Az üres listának nincs eleme, jele []. A Prolog programban a listát szokás [t1|l] alakban megadni, ahol t1 egy elem, a lista feje és l egy lista, a lista toldaléka. A Prolog belső ábrázolási módja miatt a lista elemei közül mindig az első elem az elérhető. A fontosabb listaműveletekre – elemkeresés és -törlés listában, lista hossza, két lista konkatenációja, lista fordított sorrendbe írása, stb. – a Prolog fordítókba beépített programok vannak. A rekurzív logikai programok bemutatása kapcsán mégis felsorolunk közülük néhányat.

  1. A listában egy elem keresése:

member(X,[X|Told]).

member(X,[Y|Told]) :- member(X,Told).

Egy lehetséges célklóz a :- member(e,l), ahol e a keresett elem, l pedig a lista, amiben keresünk.

  1. A listából egy elem törlése:

del(X, [X|Told], Told).

del(X, [Y|Told], [Y|Told1]) :- del(X,Told,Told1).

Egy lehetséges célklóz a :- del(e,l), ahol e az az elem, amit az l listából akarunk törölni.

  1. A lista hosszának meghatározása (feltételezzük, hogy az s(x) rákövetkezési függvény kiszámítására már rendelkezésre áll egy Prolog program):

length([],0).

length([X|Told],s(N)) :- length(Told, N).

Egy lehetséges célklóz a :- length(l,X), ahol l a lista, aminek a hoát meg akarjuk határozni, és X egy változó, melyre a válaszhelyettesítés megadja a lista hosszát.

  1. A lista utolsó elemének meghatározása:

last(X,[X]).

last(X,[Y|L]) :- last(X,L).

Egy lehetséges célklóz az :- last(X,l), ahol l a lista, aminek az utolsó elemét keressük, és X egy változó, melyre a válaszhelyettesítés megadja a lista utolsó elemét.

  1. Két lista konkatenációjának előállítása:

conc([],L,L).

conc([X|L1],L2,[X|L3]) :- conc(L1,L2,L3).

Egy lehetséges célklóz a :- conc(l1,l2,L), ahol l1 és l2 a két konkatenálandó lista, és L egy változó, melyre a válaszhelyettesítés megadja a két lista konkatenációját.

Végül példát mutatunk a ciklusszervezésre:

  1. Ciklusszervezés listával és visszalépéssel:

vcikl(L) :- member(X,L), print(X), fail.

vcikl(L).

  1. Ciklusszervezés számlálással (feltételezzük, hogy az egyszerű aritmetikai relációkra és műveletekre már rendelkezésre állnak a Prolog programok):

scikl(0).

scikl(N) :- less(0,N), minus(N,1,N1), print(N), scikl(N1).

Ezzel a klasszikus Prolog eszköztárát lényegében megismertük, bár az aritmetikai relációk és műveletek logikai programmal való definícióiról nem esett szó.

A Prolog szemantikája

Vizsgáljuk meg – a programnyelvek esetében szokásos módon – a Prolog nyelv szemantikáját. Legyen megadva egy tételbizonyítási feladat feltételformuláknak és a tétel negáltjának Skolem-normálformáiból előálló – elsőrendű Horn-klózok halmazával. Ekkor a feltételformulákból előálló elsőrendű definit programklózok sorozata egy Prolog program. Tehát a Prolog program feltételformulák halmazként jelenik meg egy olyan tételbizonyítási feladatban, ahol a tétel negáltja egy csak negált literálokat tartalmazó, elsőrendű klóz.

Deklaratív szemantika

Adott P logikai program és T tétel esetén, vajon a T formula a P formulahalmaz következményei között van-e? Más formában megfogalmazva a kérdést:

  • Ha modellje P-nek (azaz egy P-t kielégítő interpretáció), akkor modellje-e T-nek is?

  • Igaz-e, hogy P{¬T}-nek nincs modellje?

Mivel elsőrendű klózhalmazról van szó, elegendő a Herbrand-modellekkel foglalkozni. Jelölje P a P-t leíró nyelvhez tartozó Herbrand-univerzumot, P a Herbrand-bázist. A Herbrand-bázis az P feletti -beli alapatomok egy sorozata. Az P Herbrand-interpretációt az P-ben igaz alapatomok halmazával adjuk meg. Tehát PP, ami azt jelenti, hogy az összes Herbrand-interpretáció megadható, mint P hatványhalmazának egy eleme. A továbbiakban felsorolt néhány, a logikai programozás megalapozásában fontos tétel megtalálható a [4,39] könyvekben.

7.2.9. TÉTEL. Legyen P egy definit program és {i}iI a P Herbrand-modelljeinek nemüres halmaza, akkor iIi is Herbrand-modellje P-nek.

Mivel P definit klózokból áll, a P biztosan modellje. A 7.2.9. tétel miatt P összes Herbrand-modelljének metszete szintén modell.

7.2.10. DEFINÍCIÓ. A P definit program minimális modellje vagy legszűkebb modellje az P=iIi modell, ahol {i}iI a P összes Herbrand-modelljeinek halmaza.

Más megfogalmazásban akkor minimális modell, ha nem hagyható el úgy alapatom belőle, hogy a kapott interpretáció modell maradjon.

7.2.11. TÉTEL. Legyen P egy definit program. Ekkor

P = { A | A P és P A } .

BIZONYÍTÁS. Az A alapatom pontosan akkor logikai következménye P-nek, ha P{¬A} kielégíthetetlen, azaz P{¬A}-nak nincs Herbrand-modellje. P{¬A}-nak pontosan akkor nincs Herbrand-modellje, ha ¬A hamis P minden Herbrand-modelljében, azaz ha A igaz P minden Herbrand-modelljében, vagyis ha AP.

7.2.12. PÉLDA. A legszűkebb modell mint P összes alapatom-következményének halmaza:

a P program

őse(X,Y) :- szülője(X,Y).

őse(X,Y) :- szülője(X,Z), őse(Z,Y).

szülője(X,Y) :- gyereke(Y,X).

gyereke(X,Y) :- szülője(Y,X).

gyereke(b,a).

gyereke(c,b).

gyereke(d,c).

A tényklózok minden alappéldánya következmény. Ezek felhasználásával a programklózokból előálló további alapatom-következmények:

szülője(a,b).

szülője(b,c).

szülője(c,d).

Az eddigi alapatom-következmények és a rekurzív programklóz alapján megkapjuk az összes többi alapatom-következményt:

őse(a,b).

őse(b,c).

őse(c,d).

őse(a,c).

őse(b,d).

őse(a,d).

Az alábbi fogalmakra a rekurzív programklózokat is tartalmazó logikai programok minimális P modelljének kiszámításához lesz szükség ([4,39]).

Legyen U; gyönge részbenrendezett halmaz. Az 1. fejezetben definiáltuk U tetszőleges X részhalmazának alsó és felső, valamint legnagyobb alsó és legkisebb felső korlátját. Egy U; gyönge részbenrendezett halmazt teljes hálónak neveztünk (4.5.4. definíció), ha bármely nemüres X részhalmazának volt legnagyobb alsó és legkisebb felső korlátja. Jelölje most X legnagyobb alsó korlátját glb[14](X) és legkisebb felső korlátját lub[15](X). Jelölje továbbá az U; háló legnagyobb elemét, azaz lub (U)-t, és a háló legkisebb elemét, azaz glb (U)-t.

7.2.13. DEFINÍCIÓ. Legyen U; egy teljes háló és XL. Azt mondjuk, hogy Xirányított, ha X minden véges részhalmazának van olyan felső korlátja, amely eleme X-nek.

7.2.14. DEFINÍCIÓ. Legyen U; egy teljes háló és T:UU egy leképezés. A T leképezést folytonosnak nevezzük, ha T(lub (X))=lub (T(X)) minden XU irányított részhalmazra.

7.2.15. DEFINÍCIÓ. Legyen U; egy teljes háló és T:UU egy leképezés. Az aU a T leképezés fixpontja, ha T(a)=a. Azt mondjuk, hogy az a fixpont a Tlegkisebb fixpontja, ha T bármely b fixpontja esetén ab. Jelölése: lfp [16](T).

Hasonlóan definiáljuk a Tlegnagyobb fixpontját: gfp [17](T)-t.

7.2.16. DEFINÍCIÓ. Legyen U; egy teljes háló és T:UU egy leképezés. Azt mondjuk, hogy Tmonoton, ha minden olyan x,yU esetén, melyre xy, teljesül T(x)T(y) is.

7.2.17. TÉTEL. (KNASTER ÉS TARSKI FIXPONT TÉTELE.)

Legyen U; egy teljes háló és T:UU egy monoton leképezés. Ekkor T-nek van legkisebb fixpontja:

lfp   ( T ) = glb   ( { x U | T ( x ) = x } ) = glb   ( { x U | T ( x ) x } ) ,

és legnagyobb fixpontja:

gfp  ( T ) = lub   ( { x U | T ( x ) = x } ) = lub   ( { x U | x T ( x ) } ) .

Az 1. fejezetben leírtuk a transzfinit indukció és a transzfinit rekurzió elvét. Most teljes hálókra adunk meg egy rendszámoperációt transzfinit rekurzióval.

7.2.18. DEFINÍCIÓ. Legyen U; egy teljes háló és T:UU egy monoton leképezés. A T függvény Tα és Tαrendszámhatványai a következők:

T 0 = ,

T α = T ( T ( α 1 ) ) ,

ha α rákövetkező rendszám,

T α = lub   ( { T β | β α } ) ,

ha α limesz rendszám,

T 0 = ,

T α = T ( T ( α 1 ) ) ,

ha α rákövetkező rendszám,

T α = glb   ( { T β | β α } ) ,

ha α limesz rendszám.

7.2.19. DEFINÍCIÓ. Azt a legkisebb α rendszámot, amelyre lfp (T)=Tα, illetve gfp (T)=Tα, lezárási rendszámnak nevezzük.

7.2.20. TÉTEL.

Legyen U; egy teljes háló és T:UU egy monoton leképezés. Ekkor lfp (T)=Tω.

Tehát a operátor lezárási rendszáma ω. A operátor lezárási rendszámára hasonló állítás nem igaz. Később ellenpéldákon mutatjuk be ezt a tényt.

Egy P logikai program összes Herbrand-interpretációja – mint P hatványhalmaza – teljes háló. Jelölje ezt P(P). Megmutatjuk, hogy a fenti eszközök birtokában a minimális P modellt elő lehet állítani egy megfelelő monoton P(P)P(P) leképezés legkisebb fixpontjaként.

7.2.21. DEFINÍCIÓ. Legyen P egy logikai program. Definiáljuk a következőképpen a TP:P(P)P(P) leképezést: minden P(P) esetén legyen

T P ( ) = { A P | A : B 1 , , B m alapelőfordulása egy P beli programklóznak és { B 1 , , B m } } .

T P -t közvetlen következményfüggvénynek nevezzük.

P közvetlen következményfüggvényével jellemezni lehet azokat a Herbrand-interpretációkat, amelyek modelljei P-nek.

7.2.22. TÉTEL. Legyen P egy logikai program, TP a közvetlen következményfüggvénye és egy Herbrand-interpretációja. akkor és csak akkor modellje P-nek, ha TP().

BIZONYÍTÁS. akkor és csak akkor modellje P-nek, ha minden P-beli programklóz minden olyan A:B1,,Bm alapelőfordulása esetén, amikor {B1,,Bm}, az A is fennáll. Ez viszont pontosan azt jelenti, hogy TP().

7.2.23. TÉTEL. Legyen P egy logikai program. Ekkor a TP közvetlen következményfüggvény folytonos, és ezért monoton.

Mivel tetszőleges P logikai program esetén P(P); teljes háló és TP monoton leképezés, így TP rendszámhatványait a 7.2.18. definíció alapján meghatározhatjuk. Nyilván TP0= és TP0=P. A 7.2.20. tétel szerint pedig TPα lezárási rendszáma ω. Most megadunk néhány példát rendszámhatványok meghatározására. Látunk majd olyan példát is, ahol gfp (TP)TPω, de van olyan β rendszám, hogy gfp (TP)=TPβ.

7.2.24. PÉLDA. Legyen a P program a következő:

p(f(x)) :- p(x).

q(a) :- p(x).

Számítsuk ki P közvetlen következményfüggvényének értékét az , a P és a TP(P) Herbrand-interpretációkban:

  • T P ( ) = ,

  • T P ( P ) = { q ( a ) } { p ( f ( t ) ) | t P } ,

  • T P ( T P ( P ) ) = { q ( a ) } { p ( f ( f ( t ) ) ) | t P } .

Számítsunk ki most TP néhány rendszámhatványát:

  • T P 1 = T P ( T P 0 ) = T P ( ) = = lfp  ( T P ) ,

  • T P ω = { q ( a ) } ,

  • T P ( ω + 1 ) = T P ( T P ω ) = T P ( { q ( a ) } ) = = gfp  ( T P ) .

7.2.25. PÉLDA. Legyen most a P program a következő:

p(a) :- p(x), q(x).

p(f(x)) :- p(x).

q(b).

q(f(x)) :- q(x).

Egyszerű kiszámítani, hogy

  • T P ω = { q ( f n ( b ) ) | n ω } = lfp  ( T P ) ,

  • T P ω = { p ( f n ( a ) ) | n ω } { q ( f n ( b ) ) | n ω } ,

  • T P ω 2 = { q ( f n ( b ) ) | n ω } = gfp  ( T P ) .

7.2.26. PÉLDA. Végül vizsgáljuk az alábbi P programot:

q(b).

q(f(x)) :- q(x).

p(f(x)) :- p(x).

p(a) :- p(x).

r(c) :- r(x), q(x).

r(f(x)) :- r(x).

Ekkor

  • T P ω = { q ( f n ( b ) ) | n ω } = lfp  ( T P ) ,

  • T P ω = { p ( f n ( a ) ) | n ω } { q ( f n ( b ) ) | n ω } { r ( f n ( c ) ) | n ω } ,

  • T P ω 2 = { p ( f n ( a ) ) | n ω } { q ( f n ( b ) ) | n ω } = gfp  ( T P ) .

Vegyük észre, hogy gfp (TP)lfp (TP).

7.2.27. TÉTEL. Legyen P egy definit program. Ekkor

P = lfp   ( T P ) = T P ω .

BIZONYÍTÁS. A 7.2.10. definíció miatt

P = glb   ( { | a P Herbrand modellje } ) .

A 7.2.22. tétel miatt ez éppen glb ({|TP()}), de a 7.2.17. tétel miatt ez lfp (TP), azaz a 7.2.20. és a 7.2.23. tételek miatt TPω.

Összefoglalva, egy P logikai program összes alapatom-következménye alkotja P-t. Rekurzív programklózokat is tartalmazó programok esetén P-t – P összes alapatom-következményét – TP legkisebb fixpontjaként lehet elérni. Ezért szokás a deklaratív szemantikát fixpont szemantikának és a rekurzív formulákat is megengedő logikai nyelveket fixpont logikának nevezni.

Itt említjük meg a válaszhelyettesítések (7.2.8. definíció) és az P kapcsolatát tisztázó tételt, ami arról szól, hogy egy θ korrekt válasz esetén Gθ atomi formuláinak alappéldányai mikor elemei P-nek.

7.2.28. TÉTEL. Legyen P egy definit program és legyen a G definit cél:C1,,Cn. Tegyük fel, hogy θ válasz P{G}-re és (C1Cn)θ alapformula. Ekkor a következő állítások ekvivalensek:

  1. θ korrekt válasz.

  2. ( C 1 C n ) θ igaz P minden Herbrand-modelljében.

  3. ( C 1 C n ) θ igaz P-ben.

BIZONYÍTÁS. Elég belátni, hogy (c)-ből következik (a). Mivel (C1Cn)θ igaz P-ben, ebből következik, hogy (C1Cn)θ igaz P minden Herbrand-modelljében, amiből pedig az következik, hogy ¬(C1Cn)θ hamis P minden Herbrand-modelljében. Így P{¬(C1Cn)θ}-nak nincs Herbrand-modellje, azaz nincs modellje sem. Tehát (C1Cn)θ logikai következménye P-nek.

Ezzel arra az eredményre jutottunk, hogy egy A alapatom pontosan akkor következménye egy P programnak, ha AP. Ehhez kötődik a negáció kezelésére a korábban már ismertetett not X logikai program: ha AP, akkor ¬A következménye P-nek.

Eljárásalapú és kiszámítási szemantika

A továbbiakban a logikai programok eljárásalapú szemantikájával és a szintaktikai úton kapott eredmények szemantikai értelmezésével foglalkozunk.

A P definit program és a G definit célklóz egy lineáris inputrezolúciós (LD) algoritmus bemenete. Ennek megfelelően a P{G}eljárásalapú vagy procedurális szemantikája az a válasz, amit vele kapcsolatban a lineáris inputrezolúciós algoritmus eredményez, tehát a válasz arra a kérdésre, hogy P{G}-nek van-e lineáris inputrezolúciós cáfolata.

A P program és a G célklóz a lineáris inputrezolúciós algoritmus számítógépes implementációja során – a bevezetett konkrét megszorító stratégia mellett – kapott lineáris inputrezolúciós (SLD) algoritmusnak is bemenete. Ily módon a P{G}kiszámítási szemantikája az az információ, amit az implementált SLD algoritmus eredményez: egyrészt az a válasz, hogy P{G}-nek van-e SLD cáfolata, másrészt pedig azoknak az állapotoknak a jelentése, amelyeket az algoritmus a teljes levezetési fa felépítése során elérhet.

Az LD algoritmus számítógépes implementációja során a megszorító (S) stratégiát meg lehet úgy választani, hogy az SLD rezolúciós algoritmus teljes maradjon a Horn-formulák esetére. Ennek megfelelően a P{G} eljárásalapú és kiszámítási szemantikája ugyanaz.

A továbbiakban a kiszámítási szemantika második részével foglalkozunk. Az SLD algoritmus a P logikai program felhasználásával a G gyökerű teljes levezetési fát felépíti a ,,mélységben először” bejárás szerint.

7.2.29. DEFINÍCIÓ. Sikeres ágnak nevezzük a teljes levezetési fa egy ágát, ha az üres klóz levezetésével fejeződik be. Sikeres levezetési fának nevezzük a teljes levezetési fát, ha van legalább egy sikeres ága. Legyen G-ben egyetlen alapatom. A sikerhalmaz azon alapatomok halmaza, amelyekre a G gyökerű teljes levezetési fában van sikeres ág.

7.2.30. DEFINÍCIÓ. Végesen kudarcos ágnak nevezzük a teljes levezetési fa egy ágát, ha az ágon szemléltetett levezetés nem folytatható. Végesen kudarcos levezetési fának nevezzük a teljes levezetési fát, ha minden ága végesen kudarcos. Legyen G egy alapatom negáltja. A kudarchalmaz azon alapatomok halmaza, amelyekre a G gyökerű teljes levezetési fa végesen kudarcos.

Tekintsük a 7.1. és a 7.2. ábrákat, amelyek sikeres levezetési fák, de a sikeres és a végesen kudarcos ágakon kívül végtelen águk is van. A sikeres levezetési fa azt mutatja, hogy P{G}-nek van, a végesen kudarcos levezetési fa pedig azt, hogy nincs SLD cáfolata. Ha a teljes levezetési fa csak végesen kudarcos ágakat és végtelen ágakat tartalmaz, akkor a kérdésre ilyen módon nem kapunk választ.

A logikai program szemantikai és szintaktikai tulajdonságainak kapcsolata az alábbi tételekben fogalmazható meg ([4,39]).

7.2.31. TÉTEL. Legyen P egy definit program. Ekkor P sikerhalmaza éppen a TPω=P alapatom-halmaz.

Ez azt jelenti, hogy P-nek minden AP alapatom-következményére van SLD cáfolat. Most a véges kudarchalmaz elemeit jellemezzük a TP függvénnyel. Jelölje dP a d lépésben kudarcos alapatomok halmazát, azaz

  • A   1 P , ha ATP1 (A olyan alapatom, amely nem közvetlen következménye P-nek), illetve

  • A   d P (d1) minden olyan B:B1,,Bm programklózra és θ alaphelyettesítésre, ahol A=Bθ és 1km-re Bkθ d1P.

7.2.32.DEFINÍCIÓ. Legyen P egy definit program. Pvéges kudarchalmaza

P = d 1 d P

7.2.33. TÉTEL. Legyen P egy definit program. Ekkor P=PTPω.

7.2.34. TÉTEL. Legyen P egy definit program és AP. Ha P{:A} levezetési fája végesen kudarcos, ahol a mélység legfeljebb d, akkor ATPd.

7.2.35. TÉTEL. Legyen P egy definit program és AP. Ekkor a következő állítások ekvivalensek:

  1. A P , azaz A a véges kudarchalmaz eleme.

  2. A T P ω .

  3. P { : A } minden SLD levezetési fája végesen kudarcos.

A felsorolt tételek TP rendszámhatványainak P{G} szintaktikus tulajdonságaival való kapcsolatait mutatják meg. összevetve ezekkel TP rendszámhatványainak P{G} szemantikus tulajdonságaival való kapcsolatait, választ kaphatunk arra, hogy az SLD algoritmussal még milyen szemantikus kérdések kezelése lehetséges.

A negáció kezelése

Már tudjuk, hogy az SLD algoritmus nem képes kezelni :- ¬ C alakú célklózt, ezért az algoritmushoz kiegészítéseket dolgoztak ki. Ezek az algoritmusok a definit program deklaratív szemantikájánál bemutatott lehetőségeket és a kiszámítási szemantika ezeknek megfeleltethető lehetőségeit veszik figyelembe.

Tekintsük először azt az esetet, amikor P egy definit program, de a célklóz tartalmaz negált literálokat is. Láttuk, hogy P minimális Herbrand-modellje előállítható az SLD algoritmussal mint a sikerhalmaz (7.2.31. tétel). Azt is megmutattuk, hogy azokat az alapklózokat is megkeresi az algoritmus, amelyekről véges lépésben eldönthető, hogy nem következményei P-nek, ez a kudarchalmaz. A negációkezelésben ennek megfelelően két módszert dolgoztak ki. Legyen AP.

  1. A ,,zárt világ feltételezés” (CWA[18]) szabály:

Tekintsük ¬A-t bizonyítottnak, azaz P következményének, ha AP. Ha pedig AP, akkor ¬A nem következménye P-nek.

  1. A ,,negáció mint kudarc” (NF[19]) szabály:

Tekintsük ¬A-t a P program következményének, ha az A alapatom teljes levezetési fája végesen kudarcos, azaz ha AP. Tehát ha az SLD levezetésben a ¬A célliterál következik, akkor elő kell állítani :- A teljes levezetési fáját. Ha ez végesen kudarcos, akkor úgy tekintjük, hogy ¬A levezetése sikeres, és az eredeti algoritmus folytatódik. Ez a negációkezelő módszer az SLDNF rezolúciós stratégia.

7.2.36. PÉLDA. Most bemutatjuk a két módszert. Legyen a program a következő:

tanuló(béla).

tanuló(jenő).

tanuló(győző).

tanár(klára).

Azt szeretnénk belátni, hogy ,,Klára nem tanuló”, vagyis a célklóz

:- ¬ tanuló(klára).

  1. Alkalmazzuk a CWA szabályt: a példában P maga a P program, melynek tanuló(klára) nem eleme, tehát a ¬ tanuló(klára) a CWA szabály szerint következmény.

  2. Alkalmazzuk az NF szabályt: állítsuk elő a :- tanuló(klára) teljes levezetési fáját. Ez már egy lépésben kudarcos, tehát a ¬ tanuló(klára) az NF szabály szerint következmény.

7.2.37. MEGJEGYZÉS. Megjegyezzük, hogy a fenti két következtetési szabály nem monoton, hiszen az eredeti program negált következményei a program bővítése után nem feltétlenül maradnak következmények.

Tekintsük most azt az esetet, amikor a P logikai program programklózai is tartalmazhatnak negált literálokat.

7.2.38. DEFINÍCIÓ. Normál programnak nevezünk egy logikai programot, ha a programklózok A:L1,,Ln alakúak, ahol A atomi formula és L1,,Ln literálok.

Minden P normál programnak van modellje, hiszen a programklóz feje továbbra is negálatlan atomi formula. Viszont a TP közvetlen következményfüggvény nem monoton, tehát nem biztosított a normál program minimális Herbrand-modelljének létezése.

7.2.39. DEFINÍCIÓ. Egy P normál program függési gráfja olyan irányított gráf, mely csúcsai a P-ben előforduló predikátumszimbólumok és egy p csúcsból a q csúcsba pontosan akkor vezet él, ha van P-nek olyan programklóza, melynek a törzsében q és fejében p szerepel. Az élhez ¬ jelet írunk, ha a q-val képzett literál a törzsben negált.

7.2.40. DEFINÍCIÓ. Egy P normál program szintleképezése során a P-ben előforduló predikátumszimbólumokhoz természetes számokat rendelünk. Egy-egy predikátumszimbólum szintszáma a hozzárendelt természetes szám.

7.2.41. DEFINÍCIÓ. Egy P normál program rétegzett, ha van olyan szintleképezése, hogy minden P-beli programklóz esetén a törzsben előforduló

  • minden negálatlan predikátumszimbólum szintszáma kisebb vagy egyenlő,

  • minden negált predikátumszimbólum szintszáma pedig kisebb,

mint a fejben szereplő predikátumszimbólum szintszáma.

Algoritmus egy P normál programban a rétegzés megkeresésére:

  1. Kezdetben rendeljük P minden predikátumszimbólumához az 1 természetes számot.

  2. Növeljük meg P minden negált literált tartalmazó programklóza esetén a fejbeli predikátumszimbólum szintszámát 1-gyel a negált literálbeli predikátumszimbólum szintszámához képest.

  3. Ha nem kellett már átszámozni, akkor vége: a program rétegzett, egyébként az új szintszámokat átvezetjük és megismételjük a 2. lépést.

7.2.42. PÉLDA. Rétegezzük az alábbi normál programot.

q :- ¬ r.

r :- p.

r :- ¬ p.

p :- p.

A rétegzett eredmény:

lépés

p

q

r

1

1

1

1

2

2

1

3

2

A rétegzés azt biztosítja, hogy a P normál program képes definiálni a programklózok törzsében negálva szereplő atomi formulákat (azaz képes eldönteni, hogy következménye-e P-nek), mielőtt az a programklóz sorra kerülne. Rétegzett normál programok esetén ez az alapja a negált literál kezelésének: előállítjuk P függési gráfját, és rétegezzük a programot. Ha ez lehetséges, akkor a negatív literálokat már kezelni tudja az algoritmus.

Programkiegészítés és Herbrand-szabály

Egy definit vagy egy normál program programklózai csak a ,,ha …, akkor …” (,,if …then …”) alakú definíciók leírására alkalmasak. Ilyen alakban pedig nem minden esetben lehet formalizálni az ,,akkor és csak akkor, ha …” alakú definíciók ,,csak akkor, ha …” (,,only if …”) részét. Az is ismert, hogy az egyszerű ,,pozitív” kérdések megválaszolásához elegendőek a ,,ha …, akkor …” alakú programklózok is. Abban az esetben viszont, ha a tétel univerzálisan kvantált, vagy a mag nem pozitív literálok konjunkciója, akkor szükség van az ,,akkor és csak akkor, ha …” alakú definíciókra. A logikai program egy partíciója több ,,ha …, akkor …” részdefinícióval definiálja a fejben lévő literált. A definíció ,,csak akkor, ha …” részének megadásához egyetlen ,,ha …, akkor …” definícióvá alakítjuk át a partíciót, majd ennek a ,,csak akkor, ha …” részét is képezve kapjuk a kiegészített Comp(P) normál programot. Ezután valamely teljes rezolúciós stratégiával dolgozva megkapjuk a kérdésre a választ.

A programkiegészítés folyamata során az egyes partíciók fejében lévő atomi formulák termjei helyére ugyanazokat az individuumváltozókat vezetjük be, és a feltételrészben korrigáló egyenlőségekkel biztosítjuk az eredeti jelentést. Így kapjuk meg a partíciót egyetlen ,,ha …, akkor …” definícióként.

Legyen P(t1,,tn):L1,,Lm egy programklóz. A fej ,,átalakításával” és a klóz implikációs alakba írásával az

( x 1 = t 1 ) ( x n = t n ) L 1 L m P ( x 1 , , x n )

formulát kapjuk. Ha az eredeti klóz individuumváltozói y1,,yr, akkor a

y 1 y r ( ( x 1 = t 1 ) ( x n = t n ) L 1 L m ) P ( x 1 , , x n )

formula egy az eredeti klózzal ekvivalens formula. Tegyük fel, hogy a P-t definiáló partíció a programban k0 elemű. Legyenek a partícióhoz tartozó átalakított formulák rendre

E 1 P ( x 1 , , x n ) , , E k P ( x 1 , , x n ) ,

ahol Ej(1jk) általános alakja

y 1 y r ( ( x 1 = t 1 ) ( x n = t n ) L 1 L m ) .

Ekkor P-nek a Comp(P)-beli definíciója a

x 1 x n ( ( P ( x 1 , , x n ) E 1 E k ) ( E 1 E k P ( x 1 , , x n ) ) )

formula.

7.2.43. PÉLDA. Legyen a P program a következő:

nagyszülője(X,Y) :- szülője(X,Z), szülője(Z,Y).

őse(X,Y) :- szülője(X,Y).

őse(X,Y) :- szülője(X,Z), őse(Z,Y).

Legyen a kérdés egy univerzálisan kvantált formula: ,,Ős-e a nagyszülő?”, azaz feladatunk a

x y ( n a g y s z ü l ő j e ( x , y ) ő s e ( x , y ) )

kérdés megválaszolása. Ezt csak az ,,akkor és csak akkor, ha …” alak felhasználásával, és a megszokott stratégia feladásával érhetjük el. A feladat megoldásához a Comp(P)-ből elegendő a

nagyszülője(X,Y) :- szülője(X,Z), szülője(Z,Y)

programklózhoz megadni a ,,csak akkor, ha …” részt, azaz a

x y ( n a g y s z ü l ő j e ( x , y ) z ( s z ü l ő j e ( x , z ) s z ü l ő j e ( z , y ) ) ) x y ( ¬ n a g y s z ü l ő j e ( x , y ) z ( s z ü l ő j e ( x , z ) s z ü l ő j e ( z , y ) ) )

formulát. Ebből az f Skolem-függvény bevezetésével a

x y ( ¬ n a g y s z ü l ő j e ( x , y ) ( s z ü l ő j e ( x , f ( x , y ) ) s z ü l ő j e ( f ( x , y ) , y ) ) )

Skolem-formát nyerjük, majd a disztribúció alkalmazásával a

szülője(X,f(X,Y)) :- nagyszülője(X,Y).

szülője(f(X,Y),Y) :- nagyszülője(X,Y).

programklózokat kapjuk, melyekkel kiegészítjük a programot. A tétel (kérdés) negáltja a

x y ( n a g y s z ü l ő j e ( x , y ) ¬ ő s e ( x , y ) )

formula, amiből skolemizálással két klózt kapunk, ahol a és b a bevezetett Skolem-konstansok:

nagyszülője(a,b).

:- őse(a,b).

A rezolúciós levezetés során előáll az üres klóz, tehát a nagyszülő is ős:

nagyszülője(a,b).

[ célformulából ]

szülője(X,f(X,Y)) :- nagyszülője(X,Y).

[ új programklóz ]

szülője(a,f(a,b)).

[ 1, 2 rezolvense ]

:- őse(a,b).

[ célformulából ]

őse(X,Y) :- szülője(X,Z), őse(Z,Y).

[ programklóz ]

:- szülője(a,Z), őse(Z,b).

[ 4, 5 rezolvense ]

:- őse(f(a,b),b).

[ 3, 6 rezolvense ]

őse(X,Y) :- szülője(X,Y).

[ programklóz ]

:- szülője(f(a,b),b).

[ 7, 8 rezolvense ]

szülője(f(X,Y),Y) :- nagyszülője(X,Y).

[ új programklóz ]

:- nagyszülője(a,b).

[ 9, 10 rezolvense ]

[ (1, 11) rezolvense ]

Azt tudjuk, hogy egy normál P program kielégíthető, a Comp(P) azonban lehet kielégíthetetlen is. Továbbá ha Comp(P) kielégíthető lenne is, TP általában nem monoton, így az sem biztos, hogy Comp(P)-nek van minimális Herbrand-modellje, és így az eddigi eredmények nem használhatók. Arra az esetre viszont, amikor a normál program rétegezhető, fennáll a következő tétel.

7.2.44. TÉTEL. Legyen P egy rétegzett normál program. Ekkor Comp(P)-nek van minimális Herbrand-modellje.

Bár ezen eredmények alapján a negációkezelésre alkalmas a CWA és az NF szabály, kidolgoztak egy új eljárást is. A programkiegészítés és Herbrand-szabály rétegzett programra: tekintsük akkor ¬A-t a P program következményének, ha Comp (P)A-nak nincs Herbrand-modellje.

Ezzel a rezolúciós kalkuluson alapuló (Prolog típusú) logikai programozás lehetőségeit megmutató fontosabb eredményeket ismertettük. Az alábbi ábrán összefoglaljuk a negatív információ kezelésére vonatkozó lehetőségeket.

Alkalmazás

A Prolog típusú logikai programozási nyelveket alkalmazzák a relációs adatbázisokban is mint definíciós és lekérdező nyelvet. Az egyik ismert lekérdező rendszer a DATALOG. Ez mint leíró nyelv közel áll a Prologhoz. A feladatnak megfelelően a program leíró nyelve általában többfajtájú nyelv, a nyelv modellje pedig mindig valamely relációs adatbázis. éppen ezért a kérdés megválaszolásához – az illesztés helyett – relációs algebrai műveletek elvégezhetőségét kell megvizsgálni, ahogy azt az SQL lekérdező nyelv esetén is teszik. Emiatt az ismertetett problémákon kívül a kérdés szerkezetének vizsgálata is feladata az algoritmusnak. A kérdésben előfordulhat univerzális kvantor, ezért elő kell állítani a programkiegészítést: ha egy partíció több ,,ha …, akkor …” részdefinícióval adja meg a fej definícióját, a ,,csak akkor, ha …” rész megadásához a fejben lévő predikátumszimbólumok termjei helyére ugyanazokat az individuumváltozókat, a törzsbe pedig korrigáló egyenlőségeket vezetünk be. Végül ezekben az esetekben már nem lineáris inputrezolúciót, hanem valamilyen teljes rezolúciós stratégiát használunk a kérdés megválaszolására.

7.2.45. PÉLDA. Legyen az alábbi táblázat bal oszlopában látható logikai program egy adatbázis része, a jobb oszlopban pedig a partíciók feje van közös alakban:

tanít(ede,1).

tanít(X,Y) :- X=ede, Y=1.

tanít(ede,3).

tanít(X,Y) :- X=ede, Y=3.

tanít(leó,2).

tanít(X,Y) :- X=leó, Y=2.

tanít(pál,4).

tanít(X,Y) :- X=pál, Y=4.

tanít(pál,5).

tanít(X,Y) :- X=pál, Y=5.

tanár(ede).

tanár(X) :- X=ede.

tanár(leó).

tanár(X) :- X=leó.

isa(1,programozás).

isa(2,programozás).

A Comp(P) programkiegészítés

  • a tanít reláció definíciójával kapcsolatban:

( t a n í t ( x , y ) ( x = e d e y = 1 ) ( x = e d e y = 3 ) ( x = l e ó ) y = 2 ) ( x = p á l ) y = 4 ) ( x = p á l y = 5 ) ) ( ( x = e d e y = 1 ) ( x = e d e y = 3 ) ( x = l e ó y = 2 ) ( x = p á l y = 4 ) ( x = p á l y = 5 ) t a n í t ( x , y ) )

  • a tanár reláció definíciójával kapcsolatban:

( t a n á r ( x ) x = e d e x = l e ó ) ( x = e d e x = l e ó ) t a n á r ( x ) )

Legyen a kérdés: ,,Tanít-e minden tanár programozást?” A tétel negáltjából a

¬ ( x y ( t a n á r ( x ) t a n í t ( x , y ) i s a ( y , p r o g r a m o z á s ) ) ) x y ( t a n á r ( x ) ( ¬ t a n í t ( x , y ) ¬ i s a ( y , p r o g r a m o z á s ) ) )

formula áll elő, ami skolemizálva

y ( ¬ t a n á r ( s ) ( ¬ t a n í t ( s , y ) ¬ i s a ( y , p r o g r a m o z á s ) ) )

alakú. Tehát a mag nem negált literálok diszjunkciója, így egyrészt két ,,célklózhoz” jutunk:

tanár(s).

:- tanít(s,Y), isa(Y,programozás).

másrészt mivel az első literál negált, a válaszhoz szükség van a tanár és a tanít reláció ,,csak akkor, ha …” részére is, azaz a

t a n á r ( x ) x = e d e x = l e ó

formulára, ami az

X=ede, X=leó :- tanár(X).

programklózt eredményezi.

Feladatok

7.2.1. FELADAT. A Hanoi tornyai probléma a következő: Adott három oszlop: (1,2,3). Az 1-es oszlopon három különböző átmérőjű korong van csökkenő átmérő szerint egymásra téve. Rakjuk át a 3-as oszlopra a korongokat egyesével úgy, hogy az eredeti rendezés a végén megmaradjon és a korongok mozgatása során se kerüljön soha nagyobb korong kisebbre.

  1. Írjunk a feladatot megoldó logikai programot.

  2. Általánosítsuk a feladatot úgy, hogy n korongot az i-edik oszlopról a j-edik oszlopra kell átrakni, ahol ij és i,j{1,2,3}. Írjunk az általánosított feladatot megoldó logikai programot.

7.2.2. FELADAT. Legyen adva a következő logikai program:

jófilm(valamiAmerika).

jófilm(harryPotter).

jófilm(gyűrűkura).

nagyonjó(gyűrűkura).

láttukmár(harryPotter).

láttukmár(valamiAmerika).

megnézzük(X) :- láttukmár(X), nagyonjó(X).

megnézzük(X).

A megnézzük predikátum azt szeretné kifejezni, hogy ,,egy filmet akkor nézünk meg, ha még nem láttuk, vagy már láttuk ugyan, de nagyon jó a film”.

  1. Döntsük el a program segítségével, hogy nézzük-e meg a Harry Potter című filmet.

  2. Lehet-e a program írása során előre látni, hogy nem szükséges a teljes levezetési fa bejárása? Mi lesz az eredmény, ha a

megnézzük(X) :- láttukmár(X), !, nagyonjó(X).

megnézzük(X).

partíciót használjuk fel a programban?

  1. A :- megnézzük(harryPotter). kérdés esetén mi az alábbi levezetés folytatása, ha az eredeti partíciót, és mi akkor, ha a (b) pont alatti partíciót használjuk fel a programban.

:- megnézzük(harryPotter).

megnézzük(X) :- láttukmár(X), nagyonjó(X).

:- láttukmár(harryPotter), nagyonjó(harryPotter).

láttukmár(harryPotter).

:- nagyonjó(harryPotter).

nagyonjó(gyűrűkura). KUDARC

7.2.3. FELADAT. Keressük meg az alábbi programok rétegzését. Mi lesz a Comp(P) program?

r :- p.

r :- ¬ p.

p :- p.

q :- r.

r :- p.

r :- ¬ p.

p :- p.

Változtat-e a rétegzésen, ha :- q a célklóz? Mi a program következménye: q vagy ¬ q?

7.2.4. FELADAT. Mutassuk meg, hogy a ¬ p nem logikai következménye a Comp(P)-nek.

p :- ¬ q(x).

q(a).

p :- ¬ r.

r :- q(x).

q(a).



[12] Programming in Logic.

[13] Linear resolution with Selection function for Definit clauses.

[14] Greatest lower bound.

[15] Least upper bound.

[16] Least fixpoint.

[17] Greatest fixpoint.

[18] Closed World Assumption.

[19] Negation as Failure.