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.

Rezolúciós elv – rezolúciós kalkulus

Rezolúciós elv – rezolúciós kalkulus

A logika bizonyításelméleti tárgyalásához definiáltunk egy megfelelő szintaktikus következményfogalmat, majd a bizonyításelméleti levezetés előállításával mint kalkulussal megoldottuk a szintaktikus eldöntésproblémát. Megmutattuk, hogy ez a kalkulus helyes és teljes. Azt is tapasztaltuk, hogy a logikát felépíthetjük más szintaktikai eszköztár segítségével is. Minden új döntési eljárás kialakítása során a szemantikus eldöntésprobléma valamelyik alakjából indulunk ki. Megadjuk a levezetési szabályokat, és levezetésfogalmat definiálunk. Amennyiben az eljárás megköveteli, a formulákat speciális alakba írjuk át. Ezután megfogalmazunk egy szintaktikus eldöntésproblémát, meghatározva a döntési eljárás megállási feltételét. A kalkulus helyes, ha a szintaktikus eldöntésproblémára adott ,,igen” válaszból következik, hogy a szemantikus eldöntésprobléma megfelelő kérdésére is ,,igen” a válasz. A kalkulus teljes, ha minden olyan esetben, amikor a szemantikus eldöntésproblémára ,,igen” a válasz, akkor a kalkulus biztosan eléri megállási feltételét. A helyesség és a teljesség vizsgálata minden új kalkulusnál alapvető. A rezolúciós kalkulus esetén a formulahalmaz kielégíthetetlenségének igazolása a ,,háttér” szemantikus eldöntésprobléma.

Konjunktív normálformák és nulladrendű klózhalmazok

Legyenek A1,A2,,An,B(n1) tetszőleges ítéletlogikai formulák. A 4.4. fejezetből ismeretes az ítéletlogika eldöntésproblémájának két megfogalmazása:

  1. az A1A2AnB formula tautológia-e, illetve

  2. az {A1,A2,,An,¬B} formulahalmaz kielégíthetetlen-e.

Ez utóbbi halmaz formuláit átírva KNF-ba a

{ K N F A 1 , K N F A 2 , , K N F A n , K N F ¬ B }

formulahalmazt kapjuk, ami pontosan akkor kielégíthetetlen, ha a halmaz formuláiban szereplő klózok halmaza kielégíthetetlen. Tehát most a szemantikus eldöntésproblémát mint egy klózhalmaz kielégíthetetlenségének kérdését fogalmaztuk meg.

Egy nulladrendű klózhalmaz kielégíthetetlen, ha bármely interpretáció mellett van a halmaz elemei között legalább egy h igazságértékű klóz. Mivel egy klóz pontosan akkor h igazságértékű egy interpretációban, ha minden literálja is h, így azok és csak azok az interpretációk teszik h igazságértékűvé, amelyekben a klóz negált ítéletváltozói i, a negálatlanok pedig h igazságértéket vesznek fel. Egy véges klózhalmaz kielégíthetetlenségének vizsgálatára alkalmas eszköz a klózhalmazban szereplő ítéletváltozók valamely rögzített sorrendje (bázisa) mellett felépített szemantikus fa (the section called “Az ítéletlogika nyelve – szemantika” rész), ami felsorolja az összes interpretációt. A szemantikus fa éleihez literál címkéket rendeltünk. Az X címke azt jelentette, hogy az X ítéletváltozót i igazságértékkel, a ¬X címke pedig azt, hogy X-et h igazságértékkel interpretáltuk.

Legyen S egy véges klózhalmaz, és rögzítsük S ítéletváltozóinak egy bázisát. Építsük fel a bázishoz a szemantikus fát. S egy C klózának illesztése a szemantikus fára azt jelenti, hogy megkeressük az(oka)t az ága(ka)t, amelyekben minden C-beli literálnak éppen a komplemense valamely él címkéje (egy literál komplemense a literállal azonos alapú, de ellentétesen negált literál, azaz X komplemense ¬X és ¬X komplemense X). Az ezeken az ágakon megadott interpretációkban a C klóz h igazságértékű. Illesszük most az S klózhalmaz minden klózát a szemantikus fa ágaira. Ekkor azt mondjuk, hogy elkészítettük az Sklózhalmaz szemantikus fáját.

6.3.1. DEFINÍCIÓ. Egy klózhalmaz szemantikus fájának azt a csúcsát, amelybe a klózhalmaz valamely klózának illesztése során utoljára illesztett literál komplemensével címkézett él vezet, cáfoló csúcsnak nevezzük. Azt a csúcsot pedig, amelyet közvetlenül követő mindkét csúcs cáfoló csúcs, levezető csúcsnak hívjuk. A cáfoló csúcsot jelölje , a levezető csúcsot pedig .

6.3.2. DEFINÍCIÓ. Egy klózhalmaz szemantikus fájának egy ága zárt, ha cáfoló csúcsban végződik. A szemantikus fa zárt, ha minden ága zárt.

Ha egy S klózhalmaz szemantikus fája zárt, akkor a klózhalmaz kielégíthetetlen, ugyanis a klózhalmazban szereplő ítéletváltozók minden interpretációjához van olyan C klóz, amely lezárja az illető interpretációt megadó ágat, vagyis C abban az interpretációban h igazságértékű.

6.3.3. PÉLDA. Döntsük el, hogy az

S = { Y ¬ Z , X Z , ¬ X ¬ Y , ¬ X Z , ¬ Z }

klózhalmaz kielégíthetetlen-e. Készítsük el az X,Y,Z bázishoz tartozó teljes szemantikus fát:

Illesszük a ¬X¬Y klózt a szemantikus fára. A cáfoló csúcshoz a G, X1, Y1 út vezet. Ezután illesszük az S-beli többi klózt is a szemantikus fára. Látjuk, hogy a fa minden ága cáfoló csúcsban végződik:

Egy klózhalmaz szemantikus fájának mérete változhat, ha más bázist választunk. A 6.3.3. példabeli S klózhalmaz esetén válasszuk most az X,Z,Y bázist. Az S klózhalmaznak az X,Z,Y bázisra felépített szemantikus fája az alábbi ábrán látható:

Itt az is kiderül, hogy a szemantikus fa lezárásához az Y¬Z és a ¬X¬Y klózokra nincs is szükség.

6.3.4. TÉTEL.

Ha egy véges klózhalmaz szemantikus fája zárt, akkor a szemantikus fában van levezető csúcs.

BIZONYÍTÁS. Legyen az S klózhalmaz ítéletváltozóinak száma n. Tegyük fel, hogy S szemantikus fájának nincs levezető csúcsa, azaz minden (nem levél) csúcsból kiinduló két él legalább egyike nem cáfoló csúcsba vezet. Megmutatjuk, hogy a fának van nyitott ága. A gyökér (a0) nem levezető csúcs, ezért valamelyik gyereke nem cáfoló csúcs: legyen ez a1. Ha a0,a1,a2,,aj egy olyan út, amelyben egyik csúcs sem cáfoló csúcs, akkor legyen aj+1 az aj csúcsnak egy olyan gyermeke, amely nem cáfoló csúcs. Ilyen van, mert a feltevés szerint aj sem levezető csúcs. n lépés után megkapjuk a nyitott ágat.

6.3.5. MEGJEGYZÉS. Egy klózhalmaz kielégíthetetlenségének eldöntésére a továbbiakban nem a szemantikus fát fogjuk használni. A szemantikus fa azonban fontos segédeszköz marad az új kalkulus, az ún. rezolúciós kalkulus tulajdonságainak vizsgálatában. Egy ilyen fontos tulajdonság például, hogy egy levezető csúcsra illesztett két klóz pontosan egy komplemens literálpárt tartalmaz.

A rezolúciós kalkulus az ítéletlogikában

A továbbiakban az ítéletlogikának a rezolúciós kalkulussal való tárgyalását, vagyis a nulladrendű rezolúciós elvet mutatjuk be. Ez is egy szintaktikai alapokon működő döntési elv, amelynek segítségével el lehet jutni valamely ítéletlogikai formula vagy formulahalmaz kielégíthetetlenségének igazolásához, azaz a szemantikus eldöntésprobléma megoldásához.

A klózokra vonatkozó egyszerűsítési szabály szerint ha X ítéletváltozó és C egy az X-et nem tartalmazó klóz, akkor

( X C ) ( ¬ X C ) 0 C .

Az X és a ¬X egységklózok konjunkciójával ekvivalens ,,egyszerűbb” (egyetlen literált sem tartalmazó) klóz pedig a 4.5. fejezetben – a the section called “Az ítéletlogika műveleteinek tulajdonságairól” részben – bevezetett üres klóz ().

Legyenek most C1 és C2 olyan klózok, melyek pontosan egy komplemens literálpárt tartalmaznak, azaz C1=C1L1 és C2=C2L2, ahol L1 és L2 az egyetlen komplemens literálpár (C1 és C2 üres klózok is lehetnek). Világos, hogy ha a két klózban a komplemens páron kívül is vannak literálok, és ezek nem mind azonosak, az egyszerűsítési szabály alkalmazhatósági feltétele nem áll fenn. Ugyanakkor nem nehéz belátni a következő tételt.

6.3.6. TÉTEL. Ha C1=C1L1 és C2=C2L2, ahol L1 és L2 komplemens literálpár, akkor {C1,C2}0C1C2.

BIZONYÍTÁS. Be kell látni, hogy minden olyan interpretáció, amely kielégíti a {C1,C2} klózhalmazt, kielégíti a C1C2 klózt is. Világos, hogy ha C1=L1 és C2=L2, akkor nincs a {C1,C2} klózhalmazt kielégítő interpretáció, tehát igaz az állítás. Egyébként a {C1,C2} klózhalmazt kielégítő tetszőleges interpretáció

  • vagy olyan, hogy az L1-hez rendel i értéket (jelöljük ezeket L1-gyel),

  • vagy olyan, hogy az L2-höz rendel i értéket (jelöljük ezeket L2-vel).

Tekintsünk egy L1 interpretációt. L1 kielégíti a {C1,C2} klózhalmazt, tehát L1(C1)=i és L1(C2)=i, de az L1 interpretációban L1(L2)=h, ezért L1(C2)=i, tehát L1(C1C2)=i. Hasonlóképpen láthatjuk be, hogy a L2 interpretációkban L2(C1)=i. Tehát mind L1, mind L2 kielégíti a C1C2 klózt.

6.3.7. DEFINÍCIÓ. Legyenek C1 és C2 pontosan egy komplemens literálpárt tartalmazó klózok. Ha C1=C1L1 és C2=C2L2, ahol L1 és L2 a komplemens literálpár, a C1C2 klózt a (C1,C2) klózpár (vagy a C1C2 formula) rezolvensének nevezzük. Ha C1=L1 és C2=L2, rezolvensük az üres klóz.

Az a tevékenység, amelynek eredménye a rezolvens, a rezolválás, azon literálpár literáljai pedig, amely lehetővé teszi a rezolvensképzést, a kirezolvált literálok.

6.3.8. PÉLDA. Vizsgáljunk most meg néhány klózpárt, van-e rezolvensük.

klózpár

rezolvens

(a)

( X Y , ¬ Y Z )

X Z

(b)

( X ¬ Y , ¬ Y Z )

nincs: mindkét azonos alapú literál negált

(c)

( X ¬ Y , Z ¬ V )

nincs: nincs azonos alapú literál

(d)

( ¬ X ¬ Y , X Y Z )

nincs: két komplemens literálpár van

(e)

( X , ¬ X )

6.3.9. TÉTEL. Ha a C klóz a (C1,C2) klózpár rezolvense, akkor azon interpretációk a {C1,C2} klózhalmazt nem elégíthetik ki, amelyekben (C)=h.

BIZONYÍTÁS.

  • Ha C1=L1 és C2=L2, rezolvensük az üres klóz. Az üres klóz az X¬X kielégíthetetlen formula egyszerűsítése, azaz minden interpretációban hamis. Tehát azt kell belátni, hogy a {C1,C2} klózhalmaz kielégíthetetlen. De mivel C1 és C2 egy komplemens literálpár, így egyetlen interpretáció sem elégítheti ki egyszerre őket.

  • Legyen C1=C1L1 és C2=C2L2, ahol L1 és L2 komplemens literálpár. Legyen egy olyan interpretáció, amelyben (C)=h. Ez azt jelenti, hogy C1 és C2 minden literálja hamis -ben, azaz a C1 és C2 klózokban L1 és L2 kivételével minden literál hamis. Az L1 és L2 literálok közül viszont csak az egyik lehet igaz -ben, ezért a {C1,C2} klózhalmazt az interpretáció nem elégíti ki.

Ezzel a tételt bebizonyítottuk.

6.3.10. DEFINÍCIÓ. Egy S klózhalmazból a C klóz rezolúciós levezetése egy olyan véges k1,k2,,km(m1) klózsorozat, ahol minden j=1,2,,m-re

  1. vagy kjS,

  2. vagy van olyan 1s,tj, hogy kj a (ks,kt) klózpár rezolvense,

és klózsorozat utolsó tagja, km, éppen a C klóz.

Megállapodásunk szerint a rezolúciós kalkulus eldöntésproblémája az, hogy levezethető-e S-ből az üres klóz. A rezolúciós levezetés célja tehát az üres klóz levezetése S-ből. Azt, hogy S-ből levezethető az üres klóz, úgy is ki lehet fejezni, hogy S-nek van rezolúciós cáfolata.

6.3.11. PÉLDA. Próbáljuk meg az üres klózt levezetni az

S = { ¬ X Y , ¬ Y Z , X V , ¬ V Y Z , ¬ Z }

klózhalmazból. A levezetés bármelyik S-beli klózzal indítható.

1.

¬ V Y Z

[ S ]

2.

¬ Z

[ S ]

3.

¬ V Y

[ 1, 2 rezolvense ]

4.

¬ Y Z

[ S ]

5.

¬ Y

[ 2, 4 rezolvense ]

6.

¬ V

[ 3, 5 rezolvense ]

7.

X V

[ S ]

8.

X

[ 6, 7 rezolvense ]

9.

¬ X Y

[ S ]

10.

Y

[ 8, 9 rezolvense ]

11.

[ 5, 10 rezolvense ]

Tehát S-nek van rezolúciós cáfolata.

6.3.12. LEMMA. Legyen S tetszőleges klózhalmaz és a k1,k2,,km klózsorozat rezolúciós levezetés S-ből. Ekkor kj minden j=1,2,,m-re tautologikus következménye az S klózhalmaznak, azaz S0kj.

BIZONYÍTÁS.

  1. A levezetés első klóza, k1, biztosan eleme S-nek, tehát S0k1.

  2. Tegyük most fel, hogy minden jn-re igazoltuk már, hogy S0kj.

  3. Belátjuk, hogy kn+1-re is igaz az állítás. Ha kn+1S, akkor S0kn+1. Ha kn+1 valamely ks,kt klózok rezolvense, akkor a 6.3.6. tétel miatt {ks,kt}0kn+1. Az indukciós feltevés miatt S0ks és S0kt. Ebből a 4.3.3. tétel miatt S0kn+1.

Ezzel a lemmát bebizonyítottuk.

6.3.13. TÉTEL. (A REZOLÚCIÓS KALKULUS HELYESSÉGE.)

Legyen S tetszőleges klózhalmaz. Ha S-ből levezethető az üres klóz, akkor S kielégíthetetlen.

BIZONYÍTÁS. Tegyük fel, hogy van olyan interpretáció, ami kielégíti S-et. A 6.3.12. lemma szerint egy S-ből való rezolúciós levezetésbeli bármely kj klózra S0kj, tehát kielégíti a rezolúciós levezetés minden klózát is. De az üres klóz kielégíthetetlen, tehát nem lehet eleme a levezetésnek. Így tehát ha S-ből levezethető az üres klóz, akkor S kielégíthetetlen.

6.3.14. TÉTEL. (A REZOLÚCIÓS KALKULUS TELJESSÉGE.)

Ha az S véges klózhalmaz kielégíthetetlen, akkor S-ből levezethető az üres klóz.

BIZONYÍTÁS. A tételt úgy bizonyítjuk, hogy a klózhalmaz kielégíthetetlenségét feltételezve előállítjuk az üres klóz levezetését S-ből. Mint láttuk, ha S kielégíthetetlen, akkor S szemantikus fája zárt, és egy zárt szemantikus fának van legalább egy levezető csúcsa. Megmutatjuk, a zárt szemantikus fa tulajdonságainak felhasználásával, hogy a fát lezáró S klózhalmaznak mindig létezik rezolúciós cáfolata. Megadunk egy algoritmust az üres klózt eredményező rezolúciós levezetés előállítására.

  1. j : = 0 , Sj:=S, LIST:=.

  2. Állítsuk elő Sj szemantikus fáját. nj:= a szemantikus fa szintjeinek száma. Ha nj=0, akkor levezettük az üres klózt, a levezetés LIST-ből kiolvasható.

  3. Egyébként válasszuk ki a fa egy levezető csúcsát. A levezető csúcsot tartalmazó két ágra illesztett klózok legyenek kj és kj, rezolvensük pedig kj. Tegyük a LIST végére a kj,kj,kj klózokat.

  4. S j + 1 : = S j { k j } , j:=j+1. Folytassuk a 2. lépéssel.

Az algoritmus véges sok lépésben véget ér, mert minden j-re az élek száma Sj+1 szemantikus fájában kevesebb, mint Sj szemantikus fájában. Ugyanis két klóz rezolvensének hamissá válásához a két klózban szereplő ítéletváltozók közül csak a komplemens párban szereplő változóktól eltérők értékét kell rögzíteni. Ezért a levezető csúcshoz vezető ágon a rezolvenshez tartozó cáfoló csúcsba a rezolvens utolsó literáljának illesztésére használt él mutat. Ez a csúcs vagy maga a levezető csúcs, vagy egy annál magasabb szinten lévő csúcs. Vagyis ha S két klózának k rezolvensét hozzávesszük S-hez, akkor S{k} szemantikus fájában kevesebb lesz az élek száma, mint S szemantikus fájában volt. Ez biztosítja, hogy a fenti algoritmus véges számú lépésben befejeződik.

6.3.15. PÉLDA. Legyen S={X¬Z,¬XY,¬XZ,XZ,¬Y¬Z}. Adjuk meg az üres klózt eredményező rezolúciós levezetést S szemantikus fájának a segítségével.

  • S 0 szemantikus fája a Z,X,Y bázison, Q a kiválasztott levezető csúcs, n0=3:

Az első részeredmény: LIST=¬XY,¬Y¬Z,¬X¬Z|1.

  • S 1 szemantikus fája a Z,X bázison, Q a kiválasztott levezető csúcs, n1=2:

A második részeredmény:

L I S T = ¬ X Y , ¬ Y ¬ Z , ¬ X ¬ Z | 1 , ¬ X ¬ Z , X ¬ Z , ¬ Z | 2 .

  • S 2 szemantikus fája a Z,X bázison, Q a kiválasztott levezető csúcs, n2=2:

A harmadik részeredmény:

L I S T = ¬ X Y , ¬ Y ¬ Z , ¬ X ¬ Z | 1 , ¬ X ¬ Z , X ¬ Z , ¬ Z | 2 , ¬ X Z , X Z , Z | 3 .

  • S 3 szemantikus fája a Z bázison, Q a kiválasztott levezető csúcs, n3=1:

A negyedik részeredmény:

L I S T = ¬ X Y , ¬ Y ¬ Z , ¬ X ¬ Z | 1 , ¬ X ¬ Z , X ¬ Z , ¬ Z | 2 , ¬ X Z , X Z , Z | 3 , Z , ¬ Z , | 4 .

  • n 4 = 0 . A végeredmény, azaz a levezetés:

¬ X Y , ¬ Y ¬ Z , ¬ X ¬ Z , ¬ X ¬ Z , X ¬ Z , ¬ Z , ¬ X Z , X Z , Z , Z , ¬ Z , .

Előre- és visszakövetkeztetés rezolúciós kalkulussal

Minden kalkulus a tételbizonyítási feladatot oldja meg. A rezolúciós kalkulus következtetési módja a visszakövetkeztetés, hiszen a tételformula negáltja is szerepet játszik a klózhalmaz kialakításában. Legyen {A1,A2,,An} a feltételformulák halmaza és B a tételformula.

Visszakövetkeztetés: A feltételhalmazhoz hozzávesszük a tételformula negáltját és a kapott {A1,A2,,An}{¬B} formulahalmazból előállítjuk az S klózhalmazt. Ha S-nek van rezolúciós cáfolata, akkor {A1,A2,,An}0B.

6.3.16. PÉLDA. Vegyük a 4.1.21. példa (c) részében a nyomozás eredményét leíró formulahalmazt:

{ X Y , Y Z , X U , U V Z , ¬ Z } .

A nyomozók sejtését leíró ,,tételformula” ¬X. Visszakövetkeztetéshez a tétel negáltját hozzátesszük a feltételformulák halmazához, és ha a kapott formulahalmaz kielégíthetetlen, akkor igazoltuk, hogy ¬X tétel. A rezolúciós kalkulus előkészítéseként a feltételformulákból klózokat állítunk elő:

{ ¬ X Y , ¬ Y Z , X U , ¬ U ¬ V Z , ¬ Z } .

Ezt a klózhalmazt kibővítjük az X formulával (klózzal), és rezolúciós levezetéssel megpróbáljuk levezetni az üres klózt. Először adjuk meg a klózhalmaz szemantikus fáját:

A szemantikus fa alapján a levezetés:

1.

¬ X Y

[ S ]

2.

¬ Y Z

[ S ]

3.

¬ X Z

[ 1, 2 rezolvense ]

4.

¬ Z

[ S ]

5.

¬ X

[ 3, 4 rezolvense ]

6.

X

[ S ]

7.

[ 5, 6 rezolvense ]

Tehát a ¬X tétel.

Nézzük meg, hogy a rezolúciós kalkulus alkalmas-e előrekövetkeztetésre, és ha igen, hogyan lehet rezolúciós kalkulussal az előrekövetkeztetést megvalósítani.

Előrekövetkeztetés: Mivel egy S klózhalmazból való rezolúciós levezetés minden klóza szemantikus következménye S-nek, ezért ha S a feltételformulák halmazából alkotott klózhalmaz, akkor az S-ből való rezolúciós levezetés minden klóza az {A1,A2,,An} feltételhalmaz szemantikus következménye.

6.3.17. PÉLDA. Vegyük a 6.3.16. példa feltételformuláit. Azt szeretnénk tudni, hogy a jegyzőkönyvben szereplő egyszerű állítások közül melyik következménye a feltételhalmaznak. Mivel a rezolúciós levezetésben minden rezolvens (is) következménye a feltétel(klóz)halmaznak, minden a rezolúciós levezetésben szereplő literál következmény. Állítsunk elő egy rezolúciós levezetést a fenti klózhalmazból.

1.

¬ X Y

[ S ]

2.

¬ Y Z

[ S ]

3.

¬ X Z

[ 1, 2 rezolvense ]

4.

¬ Z

[ S ]

5.

¬ X

[ 3, 4 rezolvense ]

6.

X U

[ S ]

7.

U

[ 5, 6 rezolvense ]

8.

¬ Y

[ 2, 4 rezolvense ]

9.

¬ U ¬ V Z

[ S ]

10.

¬ U ¬ V

[ 4, 9 rezolvense ]

11.

¬ V

[ 7, 10 rezolvense ]

Így megkaptuk az összes literál alakú következményt: ¬Z, ¬X, U, ¬Y, ¬V. Mivel az összes ítéletváltozó előfordul a literálokban, ha több literál alakú következmény is lenne, az a kapott literálok negáltja lehetne csak, és az azt jelentené, hogy a feltételklózok halmaza kielégíthetetlen.

Rezolúciós stratégiák

Egy klózhalmazból való rezolúciós levezetés definíciója nem tartalmaz semmilyen utalást arra, hogy milyen módon lehet tartalmi vagy formai alapon valamilyen stratégiát kialakítani a rezolúciós levezetés előállítására. Az alábbiakban néhány fontosabb stratégiát ismertetünk.

Egy rezolúciós levezetés szerkezetét levezetési fa segítségével szemléltethetjük. A levezetési fa csúcsai klózok. Két csúcsból pedig pontosan akkor vezet él egy harmadik, közös csúcsba, ha ott a két klóz rezolvense található.

A 6.3.14. tétel bizonyításában leírt algoritmus egy klózhalmaz zárt szemantikus fájából előállít egy rezolúciós levezetést. Az algoritmus lépéseit követve egy levezetési fát is könnyen kaphatunk a következő módon: Tükrözzük a szemantikus fát a gyökéren átmenő vízszintes egyenesre. Írjuk a cáfoló csúcsokba az ágat lezáró klózokat. Írjuk a rezolvens klózt a rezolvens cáfoló csúcsába. Ezzel a módszerrel általában levezetési fát kapunk.

6.3.18. PÉLDA. Vegyük a 6.3.15. példa S1 klózhalmazának szemantikus fáját. Tükrözzük, és írjuk a csúcsokba a megfelelő klózokat:

A levezetési fához tartozó levezetés:

1.

X Z

[ S1 ]

2.

¬ X Z

[ S1 ]

3.

Z

[ 1, 2 rezolvense ]

4.

X ¬ Z

[ S1 ]

5.

¬ X ¬ Z

[ S1 ]

6.

¬ Z

[ 4, 5 rezolvense ]

7.

[ 3, 6 rezolvense ]

6.3.19. PÉLDA. Vizsgáljuk most a 6.3.3. példa

S = { Y ¬ Z , X Z , ¬ X ¬ Y , ¬ X Z , ¬ Z }

klózhalmazának szemantikus fáját. Tükrözzük, és írjuk a csúcsokba a megfelelő klózokat:

A levezetési fához tartozó levezetés:

1.

Y ¬ Z

[ S ]

2.

¬ X Z

[ S ]

3.

¬ X Y

[ 1, 2 rezolvense ]

4.

¬ X ¬ Y

[ S ]

5.

¬ X

[ 3, 4 rezolvense ]

6.

¬ Z

[ S ]

7.

X Z

[ S ]

8.

Z

[ 5, 7 rezolvense ]

9.

[ 6, 8 rezolvense ]

6.3.20. DEFINÍCIÓ. Egy S klózhalmazból való lineáris rezolúciós levezetés egy olyan k1,1,k2,2,,km1,m1,km rezolúciós levezetés, amelyben minden j=2,3,,m-re kj a (kj1,j1) klózpár rezolvense. A kj klózokat centrális klózoknak, az j klózokat mellékklózoknak nevezzük.

A lineáris rezolúciós levezetés definíciójából világos, hogy tetszőleges rezolúciós levezetés átírható lineárissá, azaz igaz a következő tétel:

6.3.21. TÉTEL. A lineáris rezolúciós kalkulus teljes.

A lineáris rezolúciós levezetési stratégia jól áttekinthető levezetési szerkezetet eredményez. A lineáris levezetés szerkezetét szemléltető levezetési fa a következő:

Szokás a levezetési fát egyetlen ágként (lineáris gráffal) is ábrázolni. Ekkor a centrális klózokat a csúcsokhoz, a mellékklózokat pedig az élekhez rendeljük.

Amennyiben egy levezetést lineáris gráffal ábrázolunk, a gyökérben lévő k1 klózzal kezdődő összes levezetést egyetlen fával ábrázolhatjuk. Ez a teljes levezetési fa. Egy csúcsból annyi él indul ki, ahány klózhalmazbeli klózzal, illetve a levezetés során addig előállt rezolvenssel képezhető rezolvense a csúcshoz rendelt klóznak. A teljes levezetési fa fontos eszköz annak eldöntésében, hogy létezik-e rezolúciós cáfolat az illető klózból kiindulva, hiszen a 6.3.21. tétel miatt teljes a lineáris rezolúciós kalkulus is. Ugyanis ha van az üres klóznak levezetése k1-ből, akkor azt meg is találjuk a levezetések teljes fájának bejárásával.

6.3.22. PÉLDA.

  1. Legyen S={XZ,¬XZ,X¬Z,¬X¬Z}. S-ből az XZ klózzal kezdődő egy lehetséges lineáris levezetés:

1.

X Z

[ S ]

2.

¬ X Z

[ S ]

3.

Z

[ 1, 2 rezolvense ]

4.

X ¬ Z

[ S ]

5.

X

[ 3, 4 rezolvense ]

6.

¬ X ¬ Z

[ S ]

7.

¬ Z

[ 5, 6 rezolvense ]

8.

Z

[ centrális klóz ]

9.

[ 7, 8 rezolvense ]

A levezetést szemléltető levezetési fa:

  1. Legyen S={XZ,¬XZ,¬Y¬Z,¬XY,¬Z}. Állítsunk elő egy részletet a teljes levezetési fából. Induljunk ki a XZ klózból.

Most a gyakorlatban elterjedt két jól használható, de nem teljes rezolúciós stratégiát mutatunk be. Ezek a lineáris input- és az egységrezolúciós stratégia. A két eljárás ekvivalens egymással, azaz egy klózhalmaznak pontosan akkor van lineáris inputrezolúciós cáfolata, ha van egységrezolúciós cáfolata.

6.3.23. DEFINÍCIÓ. Egy S klózhalmazból való lineáris inputrezolúciós levezetés egy olyan k1,1,k2,2,,km1,m1,km lineáris rezolúciós levezetés, amelyben minden j=1,2,,m1-re jS, azaz a lineáris input rezolúciós levezetésben a mellékklózok S-nek elemei.

6.3.24. DEFINÍCIÓ. Egy S klózhalmazból való egységrezolúciós levezetés egy olyan k1,k2,,km rezolúciós levezetés, ahol minden j=1,2,,m-re ha kjS, akkor kj két olyan őt a levezetésben megelőző ks,kt(1s,tj) klóznak a rezolvense, amelyek közül az egyik egységklóz.

Annak érzékeltetésére, hogy a lineáris inputrezolúciós stratégia nem teljes, vizsgáljuk meg a levezetési fát. Legyen a levezetésben km az üres klóz, vagyis a (km1,m1) klózpár rezolvense. m1 egységklóz és m1S, tehát S-ben kell egységklóznak lenni. Az egységrezolúció esetén pedig a levezetést el sem lehet kezdeni, ha nincs S-ben egységklóz.

6.3.25. PÉLDA. Legyen a klózhalmaz

S = { Y ¬ Z , X Z , ¬ X ¬ Y , ¬ X Z , ¬ Z } .

Egy lineáris inputcáfolat:

1.

Y ¬ Z

[ S ]

2.

¬ X Z

[ S ]

3.

¬ X Y

[ 1, 2 rezolvense ]

4.

¬ X ¬ Y

[ S ]

5.

¬ X

[ 3, 4 rezolvense ]

6.

X Z

[ S ]

7.

Z

[ 5, 6 rezolvense ]

8.

¬ Z

[ S ]

9.

[ 7, 8 rezolvense ]

A lineáris inputrezolúcióhoz tartozó levezetési fa:

Egy egységcáfolat:

1.

¬ X Z

[ S ]

2.

¬ Z

[ S ]

3.

¬ X

[ 1, 2 rezolvense ]

4.

X Z

[ S ]

5.

Z

[ 3, 4 rezolvense ]

6.

[ 2, 5 rezolvense ]

Az egységcáfolathoz tartozó levezetési fa:

Ebben a példában láttuk, hogy az S klózhalmaznak lineáris input- és egységcáfolata is van. Ez természetesen nem bizonyítja a két stratégia ekvivalenciáját. A két stratégia ekvivalenciájának bizonyítása [15]-ben található meg.

Mint azt példákon láttuk a rezolúciós kalkulust egy probléma megoldásánál úgy használjuk, hogy formalizáljuk a feltételeket és a tételt. Átírjuk a tételformula negáltját és a feltételformulákat konjunktív normálformába, a kapott klózokból rezolúciós levezetéssel megpróbáljuk levezetni az üres klózt.

Fontos, hogy a rezolúciós levezetést mindig a tételformula negáltjából kapott klózzal kezdjük. Ezzel elkerülhetjük azt az esetet, amikor a feltételhalmaz egy ,,fölösleges” formulájával kezdve a levezetést úgy adódjon, mintha az üres klóz nem lenne levezethető.

6.3.26. PÉLDA. Láttuk, hogy a 4.1.21. példa (c) részében a nyomozók sejtését leíró formula következménye a nyomozás során megállapított tényeket leíró formuláknak. Mint a 6.3.16. példában már megadtuk, a klózhalmaz

S = { ¬ X Y , ¬ Y Z , X U , ¬ U ¬ V Z , ¬ Z } { X } .

Megmutatjuk, hogy a ¬U¬VZ klózból kiindulva lineáris inputrezolúcióval az üres klóz nem vezethető le.

1.

¬ U ¬ V Z

[ S ]

2.

¬ Z

[ S ]

3.

¬ U ¬ V

[ 1, 2 rezolvense ]

4.

X U

[ S ]

5.

X ¬ V

[ 3, 4 rezolvense ]

6.

¬ X Y

[ S ]

7.

Y ¬ V

[ 5, 6 rezolvense ]

8.

¬ Y Z

[ S ]

9.

Z ¬ V

[ 7, 8 rezolvense ]

10.

¬ Z

[ S ]

11.

¬ V

[ 9, 10 rezolvense ]

A levezetés nem folytatható, hiszen nincs olyan klóz, amely tartalmazná V-t. Ez a ¬U¬VZ klózból kiinduló teljes levezetési fában szereplő bármely levezetésre érvényes.

6.3.27. MEGJEGYZÉS. Bár a lineáris inputrezolúciós stratégia nem teljes, meg lehet adni olyan formulaosztályt, amelyre az. Az olyan klózokat, amelyek legfeljebb egy nemnegált literált tartalmaznak, Horn-klózoknak nevezzük. A Horn-formulák pedig azok a formulák, melyek konjunktív normálformája Horn-klózok konjunkciója. Bebizonyították, hogy a lineáris inputrezolúciós stratégia Horn-formulák esetére (szokás azt is mondani, hogy a Horn-logikában) teljes.

Egy lineáris rezolúciós levezetés esetén nem egyszerű észrevenni, hogy a levezetés soron következő lépésében felhasználható mellékklózként egy korábbi centrális klóz. A rendezett lineáris rezolúciós levezetés egy módszer erre. Ez a módszer figyeli, hogy a központi klózokból milyen literálokat rezolváltunk már ki, és ennek ismeretében választ mellékklózt. Ezért meghatározott esetekben a rezolvensben információként megőrizzük a centrális klózból kirezolvált literált bekeretezve.

Adjuk meg az ítéletváltozók egy sorrendjét, egy bázist. Rendezett klóznak nevezünk egy klózt, ha benne a literálok alapjai a bázisban megadott sorrendben vannak. Legyenek C1 és C2 rendezett klózok. A (C1,C2) klózpárnak akkor van rendezett rezolvense, ha a C1-ből kirezolválható L1 literál a C1 utolsó literálja. A rendezett rezolvenst úgy kapjuk, hogy C1-et és C2-t egymás után írjuk, elhagyjuk a C2-ben lévő azon literálokat, amelyek a C1-ben lévő nem keretezett literálokkal megegyeznek, valamint L2-t. Ha L1-et nem követi nem keretezett literál, akkor töröljük, egyébként bekeretezzük.

Például legyen X,Y,Z a bázis, C1=XY és C2=¬YZ rendezett klózok. A (C1,C2) klózpárnak van rendezett rezolvense, mivel Y (a C1-ből kirezolválható literál) a C1 utolsó literálja. Az eredeti definíció szerint a rezolvens a XZ klóz lenne. A rendezett rezolvensben azonban feltüntetjük a C1-ből kirezolvált literált, ha azt követi nem keretezett literál. Ezért a rendezett rezolvens XYZ. A bekeretezett literálokat viszont mindig elhagyjuk, ha nem követi azokat nem keretezett literál.

6.3.28. PÉLDA. Legyen a klózhalmaz

S = { X Y , X ¬ Y , ¬ X Y , ¬ X ¬ Y } .

Induljunk ki a XY klózból. Az alábbi ábra mutatja a levezetést és az információként felsorolt literálokat:

  1. A XY klózzal indul a levezetés. A klóz utolsó literálja Y, ezért lehet X¬Y-val rezolválni ¬Y szerint. A rezolvensben Y-t kellene feltüntetni, de XY helyett X-t írunk, mivel a Y után nincs nem bekeretezett literál.

  2. A rezolvensként kapott klóz utolsó literálja X, amit lehet a ¬XY-vel rezolválni ¬X szerint. A rezolvensben van bekeretezett literál. A rezolvens XY.

  3. X Y -ban az utolsó literál Y, amit lehet a ¬X¬Y-val rezolválni, és a rezolvensbe bejegyezzük Y-t. A rezolvens XY¬X.

  4. A kapott XY¬X centrális klóznak érdekes tulajdonsága, hogy a kirezolválható literál (¬X) negáltja (X) bekeretezve szerepel benne. Ez azt jelzi, hogy a levezetésben van olyan centrális klóz, amely tartalmazza X-t, és amellyel mint mellékklózzal lehet a centrális klózt rezolválni. Amennyiben a centrális klózban csak egy nem keretezett literál van, ezzel a lépéssel megkapjuk az

Skolem-normálforma és az elsőrendű klózhalmaz

Az ítéletlogikában – a rezolúciós elv előkészítése kapcsán – a formulahalmaz kielégíthetetlenségével kapcsolatos kérdésként megfogalmazott szemantikus eldöntésproblémát egy speciális formulahalmaz, a klózhalmaz esetében vizsgáltuk. Kézenfekvő, hogy az elsőrendű logika esetén is speciális alakú zárt formulák kielégíthetetlenségének kérdésére vezessük vissza a szemantikus eldöntésproblémát.

Az automatikus tételbizonyítás egyik fontos megközelítése Herbrand nevéhez fűződik (1930). Herbrand algoritmust dolgozott ki olyan interpretáció előállítására, amely hamissá tehet egy formulát. Ugyanakkor, ha az illető formula logikailag igaz, tehát nincs olyan interpretáció, amelyben hamissá válna, ez az algoritmus véges sok lépés után megáll. A legtöbb modern automatikus tételbizonyító eljárásnak a Herbrand-módszer az alapja. 1960-ban elsőként Gilmore implementálta ezt a módszert. Az elsőrendű formulák kezelése azonban nehézségekbe ütközött. Gilmore eljárását rövid időn belül (még 1960-ban) Davis és Putnam valóban hatékonnyá alakította át. 1965-től sok eredmény született, és kialakult az elsőrendű rezolúciós elv is. Ennek alapjait Robinson [55] az elsőrendű rezolvens bevezetésével teremtette meg. Jelentős előrelépést értek el: Kowalski, Kuehner, Loveland (lineáris rezolúció), Boyer (lock rezolúció), Wos (támaszhalmaz stratégia), Chang (egységrezolúció).

Az egyszerűség kedvéért csak egyfajtájú nyelvekkel foglalkozunk. A kapott eredmények azonban érvényesek többfajtájú nyelvek esetére is.

6.3.29. DEFINÍCIÓ. Egy Q1x1Q2x2QnxnA alakú formulát prenexformulának nevezünk, ha A az [Vv] nyelv tetszőleges kvantormentes formulája és Q1,Q2,,Qn tetszőleges kvantorok (n0). A Q1x1Q2x2Qnxn szimbólumsorozat a prenexformula prefixuma, és A a prenexformula magja (vagy mátrixa). Ha a prenexformula magja konjunktív, illetve diszjunktív normálforma, akkor a formula prenex-konjunktív, illetve prenex-diszjunktív normálformula.

Megjegyezzük, hogy az ítéletlogikai fogalomhoz hasonlóan egy kvantormentes elsőrendű formula konjunktív normálforma, ha elsőrendű literálok diszjunkcióinak konjunkciója, illetve diszjunktív normálforma, ha elsőrendű literálok konjunkcióinak diszjunkciója. Továbbá elsőrendű literál minden atomi formula és az atomi formulák negáltjai. Egy elsőrendű literál alapja pedig a literálban szereplő atomi formula.

6.3.30. PÉLDA. A xy(P(x,y)¬Q(x)), a xy(P(x,y)R(x,z)), a ¬P(x,x) formulák prenexformulák, viszont a xyP(x,y)¬Q(x) formula nem prenexformula.

Tehát egy elsőrendű formula vagy prenexformula, vagy nem. Most megmutatjuk, hogy minden elsőrendű formula prenexalakra hozható, azaz minden elsőrendű formulához konstruálható vele logikailag ekvivalens prenexformula. Ennek érdekében először felsorolunk néhány, az 5.3. fejezetben is szereplő logikai ekvivalenciát, majd ismertetünk egy algoritmust, amelynek alkalmazásával tetszőleges elsőrendű formulát prenexalakra hozhatunk.

Logikai jelek közötti összefüggések:

( 1 )   ¬ ( A B ) A ¬ B

( 2 )   A B ¬ A B

Kétszeres tagadás:

( 3 )   ¬ ¬ A A

De Morgan törvényei:

( 4 )   ¬ ( A B ) ¬ A ¬ B

( 5 )   ¬ ( A B ) ¬ A ¬ B

( 6 )   ¬ x A x ¬ A

( 7 )   ¬ x A x ¬ A

Kvantorok kétoldali kiemelése:

( 8 )   x A x B x ( A B )

( 9 )   x A x B x ( A B )

Kvantorok egyoldali kiemelése:

( 10 )   Q x A B Q x ( A B )    ( x Par  ( B ) )

( 11 )   Q x A   B Q x ( A B )   ( x Par ( B ) )

Disztributivitás:

( 12 )   A   ( B C ) ( A B ) ( A C )

( 13 )   A ( B C ) ( A B ) ( A C )

A prenexalakra hozás algoritmusa

  1. A formulában szereplő implikációk és negált implikációk helyére a logikai jelek közötti összefüggések alapján a velük ekvivalens diszjunkciókat, illetve konjunkciókat írjuk.

  2. A kétszeres tagadás és De Morgan törvényeit alkalmazzuk a formulában szereplő negációkra addig, amíg minden negáció hatásköre atomi formula nem lesz.

  3. Alkalmazzuk a kétoldali kvantorkiemelésre vonatkozó logikai ekvivalenciákat.

  4. Az előző lépések eredményeképpen nyert formulához vele kongruens (az 5.3.32. tétel szerint egyúttal vele logikailag ekvivalens) változóiban tiszta formulát konstruálunk.

  5. Az egyoldali kvantorkiemelésre vonatkozó ekvivalenciákat alkalmazzuk addig, amíg az összes kvantor a formula elé nem kerül. Ezzel a formulát prenexalakra hoztuk.

  6. Prenex-konjunktív, illetve prenex-diszjunktív normálformula előállításához a kapott prenexformula magját a disztribúciót alkalmazva konjunktív, illetve diszjunktív normálformára hozzuk.

Nyilvánvaló, hogy az algoritmus véges sok lépésben véget ér, és az eredményeképpen kapott formula az eredeti formulával ekvivalens, de már prenexalakú formula, illetve prenex-konjunktív vagy prenex-diszjunktív normálformula. Az egyes lépésekben ugyanis rendre az átalakítás alatt levő formula részformuláit velük logikailag ekvivalens formulákkal helyettesítve mindig az eredeti formulával logikailag ekvivalens formulát nyerünk (5.3.40. tétel). Figyeljük meg ugyanakkor, hogy a prenexalak prefixumában a kvantorok sorrendje függ az egyoldali kvantorkiemelés lépésében a kiemelés sorrendjétől.

6.3.31. PÉLDA. Hozzuk a

x ( y P ( x , y ) y ¬ ( Q ( y ) P ( x , a ) ) ) ¬ x y ( P ( y , x ) R ( x , y ) )

formulát prenexalakra.

  1. Az implikációk átírása:

¬ ( x ( y P ( x , y ) y ( Q ( y ) ¬ P ( x , a ) ) ) ) ¬ x y ( ¬ P ( y , x ) R ( x , y ) ) .

  1. A kétszeres tagadás és De Morgan törvényeinek alkalmazása:

x ( y ¬ P ( x , y ) y ( ¬ Q ( y ) P ( x , a ) ) ) x y ( P ( y , x ) ¬ R ( x , y ) ) .

  1. Az egzisztenciális kvantor kétoldali kiemelésére vonatkozó ekvivalencia alkalmazása:

x ( y ¬ P ( x , y ) y ( ¬ Q ( y ) P ( x , a ) ) y ( P ( y , x ) ¬ R ( x , y ) ) ) .

  1. A formulában az y változó három prefixumban is meg van nevezve. Két helyen a kötött változókat szabályosan átnevezzük a formulában még nem szereplő y1 és y2 változókra:

x ( y ¬ P ( x , y ) y 1 ( ¬ Q ( y 1 ) P ( x , a ) ) y 2 ( P ( y 2 , x ) ¬ R ( x , y 2 ) ) ) .

  1. Ezután már mindegyik kvantor kiemelhető (tetszőleges sorrendben), egy lehetséges eredmény:

x y y 1 y 2 ( ¬ P ( x , y ) ( ¬ Q ( y 1 ) P ( x , a ) ) ( P ( y 2 , x ) ¬ R ( x , y 2 ) ) ) .

  1. A formula magja diszjunktív normálforma, de a disztribúció felhasználásával átírható konjunktív normálformába, ha az a további feldolgozás szempontjából úgy célszerű:

x y y 1 y 2 ( ( ¬ P ( x , y ) ¬ Q ( y 1 ) P ( x , a ) P ( y 2 , x ) ) ( ¬ P ( x , y ) ¬ Q ( y 1 ) P ( x , a ) ¬ R ( x , y 2 ) ) ) .

A 6.3.30. példában a xy(P(x,y)¬Q(x)) prenexformula prefixumában csak univerzális kvantorok vannak. Az ilyen, azaz x1x2xnA alakú formulák fontosak lesznek a továbbiakban.

6.2.32. DEFINÍCIÓ. Skolem-formulának nevezzük az olyan prenexformulát, amelynek a prefixumában csak univerzális kvantor szerepel. Ha a Skolem-formula magja konjunktív normálforma, akkor a formulát Skolem-normálformának nevezzük.

Most módszert mutatunk arra, hogyan ,,írható át” egy elsőrendű formula Skolem-formába. Miután minden elsőrendű formula prenexalakra hozható, elegendő a prenexformulák Skolem-formába ,,átírásával” foglalkozni.

Prenexformula ,,átírása” Skolem-formába

  1. Új Skolem-szimbólumok bevezetése:

Vizsgáljuk meg a x1x2xj1xjQj+1xj+1QnxnA prenexformulát, amelynek a prefixumából az egzisztenciális kvantorokat eliminálni szeretnénk. Legyen a prefixumban az első egzisztenciális kvantor a prefixum j-edik kvantora.

  • Ha j=1, azaz a prefixumban az első kvantor rögtön egy egzisztenciális, akkor nyilván minden olyan interpretációban, amikor van olyan változókiértékelés, amely mellett a formula i igazságértékű, az interpretáció U univerzumában van legalább egy uU, hogy valamely κ változókiértékelés során az x1 változóhoz éppen u-t rendeljük és κ mellett a Q2x2QnxnA formula (a x1 hatásköre) i igazságértékű lesz. Ezt az elemet Skolem-konstansnak nevezzük. Bővítsük ki az elsőrendű nyelvünket egy új s konstansszimbólummal, mely az egyes interpretációk univerzumaiban rendre egy-egy ilyen Skolem-konstanst – ha egyáltalán van ilyen – nevez meg.

  • Legyen most j1, azaz előzze meg a prefixumban az első egzisztenciális kvantort j1 számú univerzális kvantor. Egy interpretációban valamely κ változókiértékelés mellett a

x 1 x 2 x j 1 x j Q j + 1 x j + 1 Q n x n A

formula pontosan akkor igaz, ha ę-ban az x1,x2,,xj1 változókhoz bármilyen más – az interpretáció U univerzumából vett – elemet rendelve mindig van legalább egy elem U-ban, amellyel pedig az xj változót értékelve az így nyert változókiértékelés mellett a xj hatásköre (a Qj+1xj+1QnxnA formula) igazságértéke i. Azaz minden (u1,u2,,uj1)Uj1 elem j1-eshez tartozik legalább egy uU, hogy κ azon κ variánsa mellett, melyre

κ ( x ) = { u i ha x { x 1 , x 2 , , x j 1 } , u ha x = x j , κ ( x ) egyébként ,

a xj hatásköre igaz lesz. Legyen f:Uj1U egy függvény, amely minden (u1,u2,,uj1)-hez egy ilyen u értéket rendel. Ezt a függvényt Skolem-függvénynek nevezzük. Bővítsük ki az elsőrendű nyelvünket egy új fj1 aritású függvényszimbólummal (f ne szerepeljen az eredeti nyelvben). A kibővített nyelv interpretálása során az f függvényszimbólumot, ha van Skolem-függvény, Skolem-függvénnyel interpretáljuk.

  1. Kvantoreliminálási lépés:

Ezután a prefixumból elhagyjuk a xj-t, és a formula magjában elvégezzük az (xjs), illetve az (xjf(x1,x2,,xj1)) termhelyettesítést. A kapott Q2x2QnxnA(x1s), illetve

x 1 x 2 x j 1 Q j + 1 x j + 1 Q n x n A ( x j f ( x 1 , x 2 , , x j 1 ) )

formula az eredeti formulában szereplő első egzisztenciális kvantort már nem tartalmazza.

Megmutatjuk, hogy ezzel a lépéssel az eredeti formulával a kielégíthetőség szempontjából egyenértékű formulát kaptunk.

  1. Egyrészt minden olyan interpretációban, amelyben az eredeti formula valamely változókiértékelés mellett igaz volt, az új függvényszimbólumot (konstansszimbólumot) interpretálhatjuk egy Skolem-függvénnyel (Skolem-konstanssal) úgy, hogy a változókiértékelés mellett igaz lesz az átalakított formula is.

  2. Ha pedig az eredeti formula minden interpretációban, minden változókiértékelés mellett hamis volt, azaz kielégíthetetlen, akkor az átalakított formula is az lesz, mivel ekkor nincs Skolem-függvény (konstans) egyetlen interpretáló struktúrában sem. Ugyanis amennyiben egy interpretációban az eredeti formula hamis minden változókiértékelés mellett, akkor van legalább egy olyan κ változókiértékelés, hogy κ minden xj-variánsa mellett a xj hatásköre h igazságértékű. Azaz xj számára nincs olyan eleme az interpretáció U univerzumának, amellyel kiértékelve xj-t, a xj hatásköre i igazságértékű lenne. Ebben az esetben bárhogy is definiáljuk a struktúrában az f függvényszimbólumot interpretáló Uj1U függvényt (az s konstansszimbólumot interpretáló uU elemet), a

x 1 x 2 x j 1 Q j + 1 x j + 1 Q n x n A ( x j f ( x 1 , x 2 , , x j 1 ) )

(illetve Q2x2QnxnA(x1s)) formula igazságértéke minden változókiértékelés mellett hamis lesz.

  1. Az új Skolem-szimbólumok bevezetésének és a kvantoreliminálásnak a lépéseit végrehajtjuk a soron következő egzisztenciális kvantorra mindaddig, amíg minden egzisztenciális kvantort nem elimináltunk.

6.3.33. PÉLDA. Írjuk át Skolem-normálformába a 6.3.31. példában kapott

x y y 1 y 2 ( ( ¬ P ( x , y ) ¬ Q ( y 1 ) P ( x , a ) P ( y 2 , x ) ) ( ¬ P ( x , y ) ¬ Q ( y 1 ) P ( x , a ) ¬ R ( x , y 2 ) ) )

prenex-konjunktív formulát. A két egzisztenciális kvantor a prefixum első két kvantora, ezért két Skolem-konstanst kell bevezetnünk. Jelöljük az a-tól különböző két új konstanst s1 és s2-vel.

y 1 y 2 ( ( ¬ P ( s 1 , s 2 ) ¬ Q ( y 1 ) P ( s 1 , a ) P ( y 2 , s 1 ) ) ( ¬ P ( s 1 , s 2 ) ¬ Q ( y 1 ) P ( s 1 , a ) ¬ R ( s 1 , y 2 ) ) ) .

6.3.34. DEFINÍCIÓ. Elsőrendű klóznak nevezünk egy olyan zárt Skolem-formulát, amelynek a magja elsőrendű literálok diszjunkciója.

Egy Skolem-normálforma magja egy elsőrendű nyelv literáljai diszjunkcióinak konjunkciós lánca. Vegyük észre, hogy ha egy zárt K Skolem-normálformára ,,visszafelé” alkalmazzuk a konjunkcióra vonatkozó kétoldali kvantorkiemelési szabályt (8), akkor elsőrendű klózok konjunkcióját kapjuk (ami nyilván egy a K-val ekvivalens formula). Legyen S ezen klózok halmaza. A következő nyilvánvaló tételt mondhatjuk ki:

6.3.35. TÉTEL. Legyen K egy zárt Skolem-normálforma, S pedig a K magjából nyert elsőrendű klózoknak a halmaza. K pontosan akkor kielégíthetetlen, ha S kielégíthetetlen.

6.3.36. PÉLDA. A 6.3.33. példában kapott Skolem-normálformában alkalmazzuk a (8)-as kvantorkiemelésre vonatkozó ekvivalenciát ,,visszafelé”:

y 1 y 2 ( ¬ P ( s 1 , s 2 ) ¬ Q ( y 1 ) P ( s 1 , a ) P ( y 2 , s 1 ) ) y 1 y 2 ( ¬ P ( s 1 , s 2 ) ¬ Q ( y 1 ) P ( s 1 , a ) ¬ R ( s 1 , y 2 ) ) .

A formula jelentése nem változik, ha az egyik klózban a kötött változókat szabályosan átnevezzük úgy, hogy a formula változóiban tiszta legyen. Például y1 helyett írjunk x1-et, y2 helyett pedig x2-t.

y 1 y 2 ( ¬ P ( s 1 , s 2 ) ¬ Q ( y 1 ) P ( s 1 , a ) P ( y 2 , s 1 ) ) x 1 x 2 ( ¬ P ( s 1 , s 2 ) ¬ Q ( x 1 ) P ( s 1 , a ) ¬ R ( s 1 , x 2 ) ) .

Az így nyert elsőrendű változóiban tiszta klózhalmaz:

{ y 1 y 2 ( ¬ P ( s 1 , s 2 ) ¬ Q ( y 1 ) P ( s 1 , a ) P ( y 2 , s 1 ) ) , x 1 x 2 ( ¬ P ( s 1 , s 2 ) ¬ Q ( x 1 ) P ( s 1 , a ) ¬ R ( s 1 , x 2 ) ) } .

Mivel egy elsőrendű klóz minden változója univerzálisan kvantált, az elsőrendű klózhalmazokban a klózok prefixumait (helykímélési céllal) nem tüntetjük fel. Tehát a fenti elsőrendű klózhalmazt így adjuk meg:

{ ¬ P ( s 1 , s 2 ) ¬ Q ( y 1 ) P ( s 1 , a ) P ( y 2 , s 1 ) , ¬ P ( s 1 , s 2 ) ¬ Q ( x 1 ) P ( s 1 , a ) ¬ R ( s 1 , x 2 ) } .

6.3.37. MEGJEGYZÉS. Az a lehetőség, hogy egy elsőrendű klózhalmaz változóiban tisztává tehető, technikai jelentőségű. Később, az elsőrendű rezolúciós kalkulus megismerése során majd fogjuk látni ennek előnyeit.

6.3.38. PÉLDA. Írjuk át Skolem-normálformába a

x y z ( ( ¬ P ( x , y ) Q ( x , z ) ) R ( x , y , z ) )

prenexformulát. Először írjuk át a formula magját konjunktív normálformába:

x y z ( ( ¬ P ( x , y ) R ( x , y , z ) ) ( Q ( x , z ) R ( x , y , z ) ) ) .

A Skolem-függvények egyváltozósak, vezessünk be az elsőrendű nyelvbe jelölésükre két új függvényszimbólumot: f-et és g-t. A Skolem-normálforma:

x ( ( ¬ P ( x , f ( x ) ) R ( x , f ( x ) , g ( x ) ) ) ( Q ( x , g ( x ) ) R ( x , f ( x ) , g ( x ) ) ) ) .

Elsőrendű klózok konjunkciójaként felírva a formulát:

x ( ¬ P ( x , f ( x ) ) R ( x , f ( x ) , g ( x ) ) ) x ( Q ( x , g ( x ) ) R ( x , f ( x ) , g ( x ) ) ) .

A változóiban tiszta elsőrendű klózhalmaz pedig:

{ ¬ P ( x , f ( x ) ) R ( x , f ( x ) , g ( x ) ) , Q ( y , g ( y ) ) R ( y , f ( y ) , g ( y ) ) } .

A tételbizonyítási problémák rezolúciós kalkulussal történő megoldásához a feltételformulák és a negált tételformula konjunkcióját írjuk majd át Skolem-normálformába. Egy konjunkciós formulának Skolem-normálformába való átalakítását a kvantorkiemelési szabályok miatt a következőképpen érdemes elvégezni:

  1. Először írjuk át rendre a konjunkciós tagokat Skolem-normálformába.

  2. Képezzük az eredményformuláknak a konjunkcióját.

6.3.39. PÉLDA. Legyen a konjunkciós formula:

x y ( ( P ( x ) Q ( y ) ) ( Q ( y ) S ( y ) ) ) y ( R ( y ) x P ( x ) ) x ¬ S ( x ) .

  1. Írjuk át a konjunkciós tagokat Skolem-normálformába.

  • A konjunkció első tagja:

x y ( ( P ( x ) Q ( y ) ) ( Q ( y ) S ( y ) ) ) .

A mag normálformában:

x y ( ( ¬ P ( x ) Q ( y ) ) ( ¬ Q ( y ) S ( y ) ) ) .

Az f Skolem-függvény bevezetésével az egzisztenciális kvantor eliminálása:

x ( ( ¬ P ( x ) Q ( f ( x ) ) ) ( ¬ Q ( f ( x ) ) S ( f ( x ) ) ) ) .

  • A konjunkció második tagja:

y ( R ( y ) x P ( x ) ) .

Egyoldali kvantorkiemelés:

y x ( R ( y ) P ( x ) ) .

Az a Skolem-konstans bevezetésével az egzisztenciális kvantor eliminálása:

x ( R ( a ) P ( x ) ) .

  • A konjunkció harmadik tagja:

x ¬ S ( x ) .

Ez Skolem-normálforma.

  1. A három Skolem-normálforma konjunkciója:

x ( ( ¬ P ( x ) Q ( f ( x ) ) ) ( ¬ Q ( f ( x ) ) S ( f ( x ) ) ) ) x ( R ( a ) P ( x ) ) x ¬ S ( x ) .

Vegyük észre, hogy az elsőrendű klózok eléréséhez ez a formula tulajdonképpen nem is szükséges. A klózhalmaz az eredeti formula konjunkciós tagjai Skolem-normálformáiból közvetlenül is meghatározható. A

x ( ( ¬ P ( x ) Q ( f ( x ) ) ) ( ¬ Q ( f ( x ) ) S ( f ( x ) ) ) )

formula mint elsőrendű klózok konjunkciója:

x ( ¬ P ( x ) Q ( f ( x ) ) ) x ( ¬ Q ( f ( x ) ) S ( f ( x ) ) ) .

A további formulák már elsőrendű klózok. Az eredeti formula mint elsőrendű klózok konjunkciója:

x ( ¬ P ( x ) Q ( f ( x ) ) ) x ( ¬ Q ( f ( x ) ) S ( f ( x ) ) ) x ( R ( a ) P ( x ) ) x ¬ S ( x ) .

A változóiban tiszta klózhalmaz (kvantorok nélkül):

{ ¬ P ( x 1 ) Q ( f ( x 1 ) ) , ¬ Q ( f ( x 2 ) ) S ( f ( x 2 ) ) , R ( a ) P ( x 3 ) , ¬ S ( x 4 ) } .

6.3.40. PÉLDA. Állítsuk elő az elsőrendű klózhalmazt a

x y z ( ( P ( x , y ) ¬ P ( y , x ) ) ( P ( x , z ) P ( z , y ) ) )

prenexformulából. Átírjuk prenexformula magját konjunktív normálformába:

x y z ( ( ¬ P ( x , y ) ¬ P ( y , x ) ) ( P ( x , z ) P ( z , y ) ) ) .

Elimináljuk az egzisztenciális kvantort az f kétváltozós Skolem-függvény bevezetésével:

x y ( ( ¬ P ( x , y ) ¬ P ( y , x ) ) ( P ( x , f ( x , y ) ) P ( f ( x , y ) , y ) ) ) .

A formula mint elsőrendű klózok konjunkciója:

x y ( ¬ P ( x , y ) ¬ P ( y , x ) ) x y ( P ( x , f ( x , y ) ) P ( f ( x , y ) , y ) ) .

A változóiban tiszta elsőrendű klózhalmaz:

{ ¬ P ( x , y ) ¬ P ( y , x ) , P ( x 1 , f ( x 1 , y 1 ) ) P ( f ( x 1 , y 1 ) , y 1 ) } .

Az elsőrendű klózok előállításának módját megismertük. Ezután az elsőrendű klózhalmaz kielégíthetetlenségének eldöntésére keresünk eszközöket.

Az alaprezolúció

Az elsőrendű szemantika szerint egy elsőrendű klózhalmaz kielégíthetetlen, ha minden interpretációban van a klózhalmazban olyan elsőrendű klóz, amelyik hamis. Egy elsőrendű klóz hamis egy rögzített interpretációban, ha van az interpretációban olyan változókiértékelés, mely mellett a klóz magja hamis, azaz a klóz magjának különböző változókiértékelések során kapott ún. alappéldányai közül legalább egy hamis. Ez azt jelenti, hogy egy elsőrendű klózhalmaz kielégíthetetlen, ha minden interpretációban legalább egy elsőrendű klóz legalább egy alappéldánya hamis.

6.3.41. DEFINÍCIÓ. Legyen [Vv] egy elsőrendű logikai nyelv. Rögzítsünk egy U univerzumot. A nyelv egy termjének U feletti alappéldányait úgy nyerjük, hogy egy-egy κ változókiértékelés mellett a termben előforduló minden változó helyére formálisan beírunk egy a κ által a változóhoz rendelt U-beli individuumot azonosító jelet. Ha pedig a nyelv egy P(t1,t2,,tn) atomi formulájában minden ti termet kicserélünk egy rögzített κ változókiértékelés mellett nyert U feletti alappéldányára, az atomi formula egy U feletti alappéldányához jutunk.

Ugyanazon U univerzum felett egy elsőrendű nyelvet több különböző módon interpretálhatunk. Vegyük észre, hogy ugyanazzal az univerzummal rendelkező interpretációkban egy term, illetve egy atomi formula alappéldányai rendre megegyeznek, ezért beszélhetünk a term, illetve az atom U feletti alappéldányairól. A term U feletti valamely alappéldánya által jelölt individuum, illetve az atom U feletti valamely alappéldánya igazságértéke viszont nyilván az interpretációtól függ:

6.3.42. DEFINÍCIÓ. Legyen a [Vv] egy elsőrendű logikai nyelv egy U feletti interpretációja. Az f(t1,t2,,tn) termnek a κ változókiértékelés mellett kapott U feletti alappéldánya az interpretációban az |f(t1,t2,,tn)|,κU-beli individuumot jelöli. A P(t1,t2,,tn) atomi formulának a κ változókiértékeléssel nyert U feletti alappéldányáról az interpretációban azt mondjuk, hogy igaz, ha P(|t1|,κ,|t2|,κ,,|tn|,κ)=i, egyébként pedig azt mondjuk, hogy hamis.

Atomi formulák U feletti alappéldányait röviden U feletti alapatomoknak fogjuk nevezni. Egy U feletti alapliterál egy alapatom vagy annak negáltja, U feletti alapliterálok diszjunkciója az U feletti alapklóz, az egyetlen alapliterált tartalmazó alapklóz az egységalapklóz és a literált nem tartalmazó alapklóz neve most is üres klóz. A következőkben speciális alapatomoknak – a P(x1,x2,,xn) alakú atomi formulák U feletti alappéldányainak – is szerepe lesz. Ezeket az alapatomokat egyszerű alapatomoknak nevezzük.

Bázisnak nevezünk U feletti egyszerű alapatomoknak egy rögzített sorrendjét. Az adott bázishoz tartozó elsőrendű szemantikus fa egy olyan bináris fa, amelynek j-edik (1j) szintszámú csúcsa a bázis j-edik alapatomjához tartozik, és egy-egy szint minden csúcsából pontosan két él indul ki, az egyik a szinthez rendelt alapatommal, a másik ennek negáltjával van címkézve. Az A egyszerű alapatom esetén jelentse az A címke azt, hogy az interpretáció i, a ¬A címke pedig azt, hogy h igazságértéket rendel A-hoz.

Egy elsőrendű formulát leíró nyelv az az elsőrendű nyelv, amelyet az eredeti nyelvből úgy nyerünk, hogy csak azokat a predikátum-, függvény- és konstansszimbólumokat hagyjuk meg benne, melyek a formulában előfordulnak. Világos, hogy a formulát leíró nyelv predikátumszimbólumainak egy U feletti interpretációját úgy is megadhatjuk, hogy a formula U feletti egyszerű alapatomjaihoz i és h igazságértékeket rendelünk. A nyelv predikátumszimbólumainak U feletti összes interpretációja pedig ezen predikátumszimbólumokkal nyert egyszerű alapatomok valamely bázisához tartozó szemantikus fával adható meg. A leíró nyelv egy alapatomjának jelentése a predikátumszimbólumok egy rögzített interpretációjában a függvény- és konstansszimbólumoknak az interpretálásától függ, hiszen ez mutatja meg, hogy egy-egy alapterm az univerzum melyik elemét jelöli (6.3.42. definíció), és így egy-egy alapatom melyik egyszerű alapatomnak felel meg.

Legyen egy prenexformulát leíró nyelv. A formula ,,skolemizálása” során Skolem-konstansokat, illetve -függvényeket jelölő szimbólumokkal kell kibővíteni az nyelvet. A kibővített nyelv interpretálása során vesszük egy interpretációját és az interpretáció univerzumában definiáljuk a Skolem-konstansokat, -függvényeket. Technikailag ez jelenthet értéktáblával való definiálást vagy ha ez lehetséges, az univerzumbeli műveletekkel való leírást. Ha az univerzumelemek, illetőleg a megfelelő aritású függvények közül egyik sem biztosítja a Skolem-formula kielégíthetőségét, akkor abban az interpretációban a formula hamis.

Egy adott U univerzumon egy elsőrendű klózhalmaz pontosan akkor kielégíthetetlen, ha U-n a klózhalmazban szereplő klózok alappéldányainak halmaza kielégíthetetlen. Ezt úgy ellenőrizzük, hogy interpretáljuk a klózhalmaz leíró nyelvében szereplő konstans- és függvényszimbólumokat (a Skolem-konstansokat és -függvényeket jelölőket is) az összes lehetséges módon U felett. Az egyes interpretációkban előállítjuk a klózhalmazban szereplő klózok alappéldányai halmazából az egyszerű alapklózok halmazát. Ha az így nyert egyszerű alapklózhalmazok mindegyike kielégíthetetlen, akkor az alappéldányok halmaza U-n kielégíthetetlen. Az egyszerű alapklózokat ugyanúgy illesztjük a szemantikus fára, mint az ítéletlogikában. Ez azt jelenti, hogy egyszerű alapklózok egy halmaza pontosan akkor kielégíthetetlen, ha az egyszerű alapklózhalmaz szemantikus fája zárt.

6.3.43. DEFINÍCIÓ. Rögzítsünk egy U univerzumot. Legyenek K1 és K2 az U univerzum feletti egyszerű alapklózok. Azt mondjuk, hogy a K1 és K2 alapklózoknak van rezolvense, ha bennük pontosan egy komplemens alapliterálpár van, azaz K1=K1L1, K2=K2L2 és L1=¬L2. A rezolvens: a K1K2 alapklóz.

6.3.44. DEFINÍCIÓ. Egy S elsőrendű klózhalmaz klózai U feletti egyszerű alapklózainak halmazából való alaprezolúciós levezetés egy olyan véges k1,k2,,km(m1) alapklózsorozat, ahol minden j=1,2,,m-re kj

  1. vagy S-beli klóz U feletti egyszerű alapklóza,

  2. vagy van olyan 1s,tj, hogy kj a (ks,kt) alapklózpár rezolvense.

Ha egy elsőrendű klózhalmazbeli klózok alappéldányai alapján – a leíró nyelvben szereplő konstans- és függvényszimbólumok (Skolem-konstansokat és -függvényeket jelölők is) minden U feletti interpretációja mellett – előállított egyszerű alapklózhalmazból van az üres klóznak alaprezolúciós levezetése, akkor az elsőrendű klózhalmaz az adott univerzumon kielégíthetetlen. Ezzel a probléma megoldását – rögzített univerzum esetén – visszavezettük az ítéletlogikában megismert rezolúciós kalkulusra. Hangsúlyozzuk ugyanakkor, hogy alaprezolúcióval csak azt lehet eldönteni, hogy a klózhalmaz kielégíthetetlen-e adott számosságú univerzumon. Ugyanis ha egy klózhalmaz kielégíthetetlen egy adott számosságú U univerzumon, akkor minden olyan univerzumon, melynek számossága megegyezik U számosságával, szintén kielégíthetetlen. Ennek bizonyítására nem térünk ki, az olvasóra bízzuk. Viszont ezért csak akkor mondhatjuk, hogy egy klózhalmaz kielégíthetetlen, ha minden számosság esetén levezethető alaprezolúcióval az üres klóz.

6.3.45. PÉLDA. Foglalkozzunk újból a 6.3.40. példabeli

x y z ( ( P ( x , y ) ¬ P ( y , x ) ) ( P ( x , z ) P ( z , y ) ) )

formulával. Bebizonyítjuk, hogy a formula nem elégíthető ki kételemű univerzumon, de háromelemű univerzumon már kielégíthető.[9]

  1. Legyen U={a,b}. A P(a,a),P(b,b),P(a,b),P(b,a) bázishoz tartozó teljes szemantikus fát a következő ábra mutatja.

A 6.3.40. példában megadtuk a formulához tartozó

S = { ¬ P ( x , y ) ¬ P ( y , x ) , P ( x , f ( x , y ) ) P ( f ( x , y ) , y ) }

klózhalmazt. Írjuk fel a klózok alappéldányait U felett:

x

y

¬ P ( x , y ) ¬ P ( y , x )

P ( x , f ( x , y ) ) P ( f ( x , y ) , y )

a

a

1.

¬ P ( a , a )

2.

P ( a , f ( a , a ) ) P ( f ( a , a ) , a )

b

b

3.

¬ P ( b , b )

4.

P ( b , f ( b , b ) ) P ( f ( b , b ) , b )

a

b

5.

¬ P ( a , b ) ¬ P ( b , a )

6.

P ( a , f ( a , b ) ) P ( f ( a , b ) , b )

b

a

7.

¬ P ( b , a ) ¬ P ( a , b )

8.

P ( b , f ( b , a ) ) P ( f ( b , a ) , a )

Ezután interpretáljuk a ,,skolemizálás” során bevezetett f függvényszimbólumot az összes lehetséges módon. Ha az egyszerű alapklózok halmaza minden esetben kielégíthetetlen, akkor az S klózhalmaz az U univerzumon kielégíthetetlen. A vizsgálatot részben a szemantikus fa lezárásával, részben alaprezolúcióval végezzük el.

  1. Legyen először f(a,a)=a és f(b,b)=b. Ekkor a P(x,f(x,y))P(f(x,y),y) klóz egyik alappéldánya (2.) éppen P(a,a)P(a,a), ami egyszerűsítés után P(a,a), egy másik alappéldánya (4.) pedig P(b,b)P(b,b), egyszerűsítés után P(b,b).

A szemantikus fa a ¬P(a,a) és P(a,a) vagy a ¬P(b,b) és P(b,b) alapklózok illesztésével lezárható, ahogyan azt az alábbi ábrákon láthatjuk.

Figure 6.13. Az interpretációhoz tartozó zárt szemantikus fák

Az interpretációhoz tartozó zárt szemantikus fák

  1. Legyen másodjára f(a,a)=b és az f(b,b)=a. Ekkor 2-ből a P(a,b)P(b,a) egyszerű alapklózt, 4-ből pedig a P(b,a)P(a,b) egyszerű alapklózt nyerjük. Ezek a klózok egymástól csak a literálok sorrendjében különböznek.

    • Ha most f(a,b)=a, akkor 6-ból a P(a,a)P(a,b) egyszerű alapklóz áll elő, jelöljük ezt 6-vel. Végezzük el a lehetséges rezolválásokat.

9.

P ( a , b )

[ 1, 6 rezolvense ]

10.

¬ P ( b , a )

[ 5, 9 rezolvense ]

Abban az interpretációban, melyben f(b,a)=a, 8-ból előállítva a P(b,a)P(a,a) egyszerű alapklózt jelöljük ezt 8-vel. Most tovább folytatva a lehetséges rezolválásokat 10-től, megkapjuk az üres klózt.

11.

P ( a , a )

[ 8, 10 rezolvense ]

12.

[ 1, 11 rezolvense ]

Ha pedig abban az interpretációban dolgozunk, melyben f(b,a)=b, akkor a 8-ból a P(b,b)P(b,a) egyszerű alapklóz lesz; legyen ez 8. Másik ágon folytatva a lehetséges rezolválásokat 10-től, most is az üres klózhoz jutunk.

1 1 .

P ( b , a )

[ 3, 8 rezolvense ]

1 2 .

[ 10, 11 rezolvense ]

Másrészt ha szemantikus fa segítségével végezzük a vizsgálatot ebben az interpretációban, akkor az alábbi ábrán látható zárt szemantikus fát nyerjük.

Figure 6.14. A zárt szemantikus fa

A zárt szemantikus fa

  • Hasonlóan láthatjuk be a többi kételemű univerzum feletti interpretáció esetén is, hogy az épp vizsgált interpretáció nem elégítheti ki az S klózhalmazt. Tehát S kielégíthetetlen kételemű struktúrákon.

2. Megmutatjuk viszont, hogy van olyan háromelemű univerzum, amelyik az S klózhalmazt kielégíti. Ez azt jelenti, hogy van legalább egy olyan kétváltozós Skolem-függvény (az f függvényszimbólum interpretáltja) ezen univerzum felett, amely mellett S egyszerű alapklózai halmazából nem vezethető le az üres klóz.

A klózok U={a,b,c} feletti alappéldányai és egy ,,megfelelő” Skolem-függvény az alábbi táblázatban látható.

x

y

¬ P ( x , y ) ¬ P ( y , x )

P ( x , f ( x , y ) ) P ( f ( x , y ) , y )

f ( x , y )

a

a

¬ P ( a , a )

P ( a , f ( a , a ) ) P ( f ( a , a ) , a )

c

b

b

¬ P ( b , b )

P ( b , f ( b , b ) ) P ( f ( b , b ) , b )

a

c

c

¬ P ( c , c )

P ( c , f ( c , c ) ) P ( f ( c , c ) , c )

b

a

b

¬ P ( a , b ) ¬ P ( b , a )

P ( a , f ( a , b ) ) P ( f ( a , b ) , b )

a

b

a

¬ P ( b , a ) ¬ P ( a , b )

P ( b , f ( b , a ) ) P ( f ( b , a ) , a )

c

a

c

¬ P ( a , c ) ¬ P ( c , a )

P ( a , f ( a , c ) ) P ( f ( a , c ) , c )

b

c

a

¬ P ( c , a ) ¬ P ( a , c )

P ( c , f ( c , a ) ) P ( f ( c , a ) , a )

c

b

c

¬ P ( b , c ) ¬ P ( c , b )

P ( b , f ( b , c ) ) P ( f ( b , c ) , c )

b

c

b

¬ P ( c , b ) ¬ P ( b , c )

P ( c , f ( c , b ) ) P ( f ( c , b ) , b )

a

Érdekességképpen megjegyezzük, hogy ha a {0,1,2};*;+;2 struktúrával interpretáljuk a formula leíró nyelvét, akkor a Skolem-függvény leírható termmel. Interpretálja P-t a * reláció (a ciklikus közvetlen rákövetkezés: 0*1*2*0), legyen + a modulo 3 összeadás, a 2 a 2 kitüntetett elem, ekkor az f(x,y)=y+2. Ezt könnyű ellenőrizni, ha a táblázat utolsó oszlopát a0,b1,c2 megfeleltetés mellett megvizsgáljuk.

Formulák szemantikus tulajdonságai és az univerzum számossága

Alaprezolúcióval egy S elsőrendű klózhalmaz kielégíthetetlenségét csak egy adott számosságú univerzum felett lehet eldönteni. Felmerül a kérdés, hogy ha egy formula egy adott számosságú univerzumon kielégíthető, kielégíthetetlen vagy logikailag igaz, akkor mit lehet tudni a formula egy-egy szemantikus tulajdonságáról más számosságú univerzumon. Ismertetünk két érdekes eredményt egyenlőségjel-mentes nyelvek és véges univerzum esetére.

6.3.46. DEFINÍCIÓ. Legyen A a [Vv] nyelv formulája. Azt mondjuk, hogy Aazonosan igaz az U univerzumon, ha [Vv] minden U feletti interpretációjában minden κ változókiértékelés mellett |A|,κ=i.

6.3.47. LEMMA. Ha az [Vv] nyelv egy A formulája azonosan igaz valamely nN0 számosságú U univerzumon, akkor bármely n-nél kisebb számosságú Z univerzumon is azonosan igaz.

BIZONYÍTÁS. Legyen A azonosan igaz az n elemszámú univerzumon, és legyen Z számossága m, ahol mn. Tekintsük U-nak egy m számosságú U részhalmazát. Megmutatjuk, hogy A azonosan igaz U-n is és emiatt Z-n is. Legyen aU tetszőlegesen rögzítve és definiáljuk a φ:UU leképezést a következőképpen:

φ ( x ) { x ha x U , a egyébként .

Legyen az [Vv] nyelv egy tetszőleges U feletti interpretációja. Definiáljunk segítségével egy U feletti interpretációt a következőképpen: ha P a nyelv egy k aritású predikátumszimbóluma, akkor legyen

P ( x 1 , x 2 , , x k ) P ( φ ( x 1 ) , φ ( x 2 ) , , φ ( x k ) ) ,

és ha f a nyelv egy k aritású függvényszimbóluma, akkor legyen

f ( x 1 , x 2 , , x k ) f ( φ ( x 1 ) , φ ( x 2 ) , , φ ( x k ) )

minden x1,x2,,xkU esetén.

Mivel A azonosan igaz U-n, minden U feletti interpretációban, így az -ben is, minden κ változókiértékelés mellett |A|,κ=i. Az elsőrendű termekre és formulákra vonatkozó szerkezeti indukció elvét felhasználva könnyen belátható, hogy -ben minden κ változókiértékelés mellett |A|,κ=i. De -t U felett tetszőlegesen választhattuk, ezért A azonosan igaz az U univerzum felett.

6.3.48. LEMMA. Ha az A formula kielégíthető valamely nN0 számosságú U univerzumon, akkor bármely n-nél nagyobb számosságú Z univerzumon is kielégíthető.

BIZONYÍTÁS. Tegyük fel, hogy A kielégíthetetlen egy n-nél nagyobb számosságú Z univerzumon. Ebben az esetben ¬A azonosan igaz Z-n. A 6.3.47. lemma miatt ekkor ¬A azonosan igaz U-n is. Ebben az esetben viszont A nem lehetne kielégíthető U-n.

A következő tétel a logikában igen fontos és tetszőleges elsőrendű nyelv esetén érvényes. A tételt itt nem bizonyítjuk, de a tablómódszer keretein belül visszatérünk rá.

6.3.49. TÉTEL. (LÖWENHEIM ÉS SKOLEM TÉTELE.) Egy elsőrendű logikai formula pontosan akkor elégíthető ki, ha már legfeljebb megszámlálható univerzumon kielégíthető.

A Herbrand-univerzum és az elsőrendű klózhalmazok

Mivel az összes univerzumon alaprezolúcióval dönteni lehetetlen feladat, jó lenne, ha létezne olyan speciális univerzum, hogy egy S elsőrendű klózhalmaz pontosan akkor lenne kielégíthetetlen, ha kielégíthetetlen ezen univerzum felett. Egy ilyen univerzum létezését mutatta meg Herbrand, amelyet ezért Herbrand-univerzumnak neveznek. A Herbrand-univerzumot mindig az adott elsőrendű klózhalmaz alapján, azaz a klózhalmazt leíró nyelvhez állítjuk elő. Újból felhívjuk a figyelmet arra, hogy a klózhalmaz leíró nyelvének szimbólumai között a Skolem-konstansokat és -függvényeket jelölő szimbólumok is ott vannak.

Adjuk meg először az egyszerű alapatom mintájára az egyszerű alapterm fogalmát: Egy f függvényszimbólumhoz tartozó U feletti egyszerű alaptermek az f(x1,x2,,xn) alakú term U feletti alappéldányai.

A Herbrand-univerzum előállítása

Legyen S tetszőleges klózhalmaz, a leíró nyelve pedig Pr,Fn,Cnst.

  1. 0 { C n s t , ha C n s t , { a } egyébként ,  továbbá i:=0.

  2. i + 1 i T i , ahol

T i { t | t valamely f F n i feletti egyszerű alaptermje } ,

i : = i + 1 és ismételjük meg a lépést.

  1. i = 0 i .

A halmaz az S klózhalmaz Herbrand-univerzuma. Egy S klózhalmaz Herbrand-univerzuma tehát S leíró nyelvének konstansszimbólumaiból (ha ilyen nincs, egy extra szimbólumból) és függvényszimbólumaiból előállítható összes alaptermek halmaza.

6.3.50. MEGJEGYZÉS. Egy interpretáció univerzuma legalább egyelemű, vagy legalább annyi elemet tartalmaz, ahány konstansszimbólum szerepel az általa interpretált nyelvben. A Herbrand-univerzum előállításánál figyelembe vettük ezt: ha S nem tartalmazott konstansszimbólumot, akkor felvettünk egy a extra szimbólumot az univerzumba. Ez azt jelenti, hogy a Herbrand-univerzumban mindig szerepel legalább egy elem.

6.3.51. PÉLDA. Legyen S={P(a),¬P(x)P(f(x))}. Ekkor

0 = { a } ,

1 = { a , f ( a ) } ,

2 = { a , f ( a ) , f ( f ( a ) ) } ,

= { a , f ( a ) , f ( f ( a ) ) , f ( f ( f ( a ) ) ) ,... } .

6.3.52. PÉLDA. Legyen S={P(x)Q(x),R(z),T(y)¬W(y)}. Mivel S-ben nincs konstansszimbólum, ezért legyen 0={a}. S-ben függvényszimbólum sincs, ezért

0 = 1 = = = { a } .

6.3.53. PÉLDA. Legyen S={P(f(x),a,g(y),b)}. Ekkor

0 = { a , b }

1 = { a , b , f ( a ) , f ( b ) , g ( a ) , g ( b ) }

2 = { a , b , f ( a ) , f ( b ) , g ( a ) , g ( b ) ,

f ( f ( a ) ) , f ( f ( b ) ) , f ( g ( a ) ) , f ( g ( b ) ) , g ( f ( a ) ) , g ( f ( b ) ) , g ( g ( a ) ) , g ( g ( b ) ) }

Vegyük észre, hogy egy elsőrendű klózhalmaz Herbrand-univerzuma a konstrukció miatt olyan, hogy a Herbrand-univerzum feletti tetszőleges alapatom egyúttal egyszerű alapatom.

6.3.54. DEFINÍCIÓ. Legyen S egy elsőrendű klózhalmaz és a klózhalmazhoz tartozó Herbrand-univerzum. A Herbrand-univerzum feletti (egyszerű) alapatomok rögzített sorrendjét Herbrand-bázisnak nevezzük.

6.3.55. DEFINÍCIÓ. Legyen az S klózhalmaz leíró nyelve Pr,Fn,Cnst, Herbrand-univerzuma pedig . S leíró nyelve Herbrand-interpretációinak nevezzük és -vel jelöljük a nyelv azon interpretációit, melyek univerzuma éppen ,

  • minden cCnst konstansszimbólumhoz a c univerzumelemet (önmagát) rendeli, és

  • minden k aritású fFn függvényszimbólumhoz hozzárendeli azt az f:k műveletet, amelyikre minden h1,h2,,hk esetén

f ( h 1 , h 2 , , h k ) = f ( h 1 , h 2 , , h k ) .

Egy S elsőrendű klózhalmaz Herbrand-interpretációi tehát csak az S-ben előforduló predikátumszimbólumok interpretálásában különböznek.

Világos, hogy ha adva van az S elsőrendű klózhalmaz egy Herbrand-interpretációja, azt a következő módon is leírhatjuk: legyen {A1,A2,} az S klózhalmaz Herbrand-bázisa és legyen

L i { A i , ha A i igaz ban , ¬ A i , ha A i hamis ban .

Ekkor a Herbrand-interpretációt az {L1,L2,} alapliterál-halmaz egyértelműen megadja.

6.3.56. PÉLDA. Legyen S={P(x)Q(x),R(f(y))}. S Herbrand-univerzuma:

= { a , f ( a ) , f ( f ( a ) ) , f ( f ( f ( a ) ) ) , } .

S Herbrand-bázisa:

{ P ( a ) , Q ( a ) , R ( a ) , P ( f ( a ) ) , Q ( f ( a ) ) , R ( f ( a ) ) , } .

Néhány Herbrand-interpretáció:

1

=

{ P ( a ) , Q ( a ) , R ( a ) , P ( f ( a ) ) , Q ( f ( a ) ) , R ( f ( a ) ) , }

2

=

{ ¬ P ( a ) , ¬ Q ( a ) , ¬ R ( a ) , ¬ P ( f ( a ) ) , ¬ Q ( f ( a ) ) , ¬ R ( f ( a ) ) , }

3

=

{ P ( a ) , Q ( a ) , ¬ R ( a ) , ¬ P ( f ( a ) ) , Q ( f ( a ) ) , ¬ R ( f ( a ) ) , }

Az alábbi ábrán látható szemantikus fán bejelöltük az 1,2,3 Herbrand-interpretációkat.

6.3.57. DEFINÍCIÓ. Legyen az S klózhalmaz leíró nyelve Pr,Fn,Cnst, és legyen ennek valamely U univerzum feletti interpretációja. Az -nek megfelelő Herbrand-interpretációS-nek egy olyan Herbrand-interpretációja, amelyre teljesül, hogy van olyan φ:U függvény, hogy a P(h1,h2,,hn) (egyszerű) alapatom pontosan akkor igaz -ban, ha a P(φ(h1),φ(h2),,φ(hn)) egyszerű alapatom igaz -ben.

Most megmutatjuk, hogy valamely S elsőrendű klózhalmaz leíró nyelvének tetszőleges interpretációjához van megfelelő Herbrand-interpretáció.

Legyen =Pr,Fn,Cnst, ahol az interpretáció univerzuma U. Legyen a φ:U a következőképpen definiálva:

  • ha Cnst=, akkor a -ben szereplő extra konstanshoz φ rendeljen tetszőleges U-beli elemet,

  • minden cCnst (egyúttal c) konstansszimbólum esetén φ(c) legyen az Cnst(c)U-beli elem,

  • ha pedig hf(h1,h2,,hk) alakú, akkor φ(f(h1,h2,,hk)) legyen a f(φ(h1),φ(h2),,φ(hk))U-beli elem.

Most megadunk egy olyan Herbrand-interpretációt, melyben a P(h1,h2,,hn) alapatom pontosan akkor igaz, ha a P(φ(h1),φ(h2),,φ(hn)) egyszerű alapatom igaz -ben. Tekintsük az S-hez tartozó Herbrand-bázist. Ha az A1-nek megfelelő -beli alapatom igaz, a Herbrand-interpretációt megadó alapliterálhalmazba írjuk be A1-et, egyébként pedig a ¬A1 literált. Tegyük fel, hogy a Herbrand-bázis első k alapatomjához – A1,A2,,Ak-hoz – már sikerült rögzíteni az igazságértékeket az alapliterálhalmaz segítségével. Miután Ak+1 igazságértékét még nem rögzítettük (a bázis elemei különbözőek), Ak+1 is ,,megkaphatja” a neki megfelelő -beli alapatom igazságértékét.

6.3.58. PÉLDA. Legyen S={P(x),Q(y,f(y,a))} és U={1,2}. Legyen a következő: az a interpretáltja 2, a predikátum- és függvényszimbólumokhoz pedig az alábbi reláció- és művelettáblákkal definiált relációkat és műveleteket rendeli .

P

1

2

i

h

Q

1

2

1

h

h

2

i

i

f

1

2

1

1

2

2

2

1

S Herbrand-univerzuma:

= { a , f ( a , a ) , f ( a , f ( a , a ) ) , f ( f ( a , a ) , a ) , f ( f ( a , a ) , f ( a , a ) ) , } .

S Herbrand-bázisa:

{ P ( a ) , Q ( a , a ) , P ( f ( a , a ) ) , Q ( a , f ( a , a ) ) , Q ( f ( a , a ) , a ) , } .

Ekkor a φ:U megfeleltetés:

a 2 ( kötelező ) , f ( a , a ) 1, f ( a , f ( a , a ) ) 2, f ( f ( a , a ) , a ) 2, .

Az -nek megfelelő Herbrand-interpretáció:

= { ¬ P ( a ) , Q ( a , a ) , P ( f ( a , a ) ) , ¬ Q ( a , f ( a , a ) ) , Q ( f ( a , a ) , a ) , } .

6.3.59. PÉLDA. Legyen S={P(x),Q(y,f(y,z))}. Vegyük észre, hogy S leíró nyelve a 6.3.58. példabeli leíró nyelvtől csak abban különbözik, hogy ebben nincs konstansszimbólum. Interpretáljuk a S nyelvét az interpretációval, ami csak annyiban különbözik -től, hogy konstansszimbólumot nyilván nem kell interpretálnia.

Most a φ:U megfeleltetés során a-hoz bármely univerzumelem hozzárendelhető. Tartsuk meg a többi Herbrand-univerzumbeli elemre a 6.3.58. példabeli megfeleltetést.

  • Ha a2, akkor az -nek megfelelő Herbrand-interpretáció a fenti .

  • Ha a1, az -nek megfelelő Herbrand-interpretáció

= { P ( a ) , ¬ Q ( a , a ) , P ( f ( a , a ) ) , ¬ Q ( a , f ( a , a ) ) , ¬ Q ( f ( a , a ) , a ) , } .

6.3.60. TÉTEL. Ha egy interpretáció kielégít egy S elsőrendű klózhalmazt, akkor az -nek megfelelő Herbrand-interpretáció is kielégíti S-t. (Más megfogalmazásban: ha S-nek van modellje, akkor van Herbrand-modellje is.)

BIZONYÍTÁS. A 6.3.57. definíció szerint ha az -nek megfelelő Herbrand-interpretáció, akkor van olyan φ:U függvény, hogy az ugyanazt az igazságértéket rendeli P(φ(h1),φ(h2),,φ(hn))-hez, mint az a P(h1,h2,,hn)-hez minden h1,h2,,hn esetén.

6.3.61. TÉTEL. Egy S elsőrendű klózhalmaz akkor és csak akkor kielégíthetetlen, ha S-t nem elégíti ki a Herbrand-univerzuma feletti egyetlen Herbrand-interpretáció sem. (Más megfogalmazásban: S pontosan akkor kielégíthetetlen, ha nincs Herbrand-modellje.)

BIZONYÍTÁS.

  1. Tegyük fel, hogy S kielégíthetetlen. Ekkor definíció szerint S-t nem elégítheti ki (semmilyen univerzum felett) egyetlen interpretáció sem, így egyetlen Herbrand-interpretáció sem.

  2. Tegyük fel, hogy S ugyan kielégíthetetlen az általa meghatározott Herbrand-univerzumon, de S nem kielégíthetetlen, azaz van olyan U univerzum és interpretáció, amely S-t kielégíti. Legyen a -nek megfelelő Herbrand-interpretáció. A 6.3.60. tétel miatt kielégíti S-t, pedig a Herbrand-univerzum feletti interpretáció. Ellentmondásra jutottunk, tehát ha S kielégíthetetlen a Herbrand-univerzumán, akkor S kielégíthetetlen.

Ezzel a tételt bebizonyítottuk.

6.3.62. MEGJEGYZÉS. Fontos tisztázni, hogy sem a 6.3.60. tétel, sem a 6.3.61. tétel nem áll fenn, ha S nem elsőrendű klózhalmaz. Vagyis, ha S tetszőleges zárt formulák halmaza, akkor általában nem igaz, hogy S kielégíthetetlenségének vizsgálata esetén elég lenne S-et csak a Herbrand-struktúrákkal interpretálni. Például legyen S={P(a),x¬P(x)}. Az S második formulája nem elsőrendű klóz. S Herbrand-univerzuma: ={a}, S Herbrand-bázisa: {P(a)}. Az S formulahalmazt egyik Herbrand-interpretáció sem elégíti ki. Azonban S kielégíthető, hiszen az az U={0,1} feletti interpretáció, melyben P(0)=i, P(1)=h és a0, kielégíti S-et.

Most ismertetjük az elsőrendű rezolúciós kalkulushoz is elvezető Herbrand-tételeket.

6.3.63. TÉTEL. (HERBRAND TÉTELE, 1. VÁLTOZAT)

Egy S elsőrendű klózhalmaz akkor és csak akkor kielégíthetetlen, ha a klózhalmaznak bármely Herbrand-bázisához tartozó teljes szemantikus fához van legalább egy véges zárt szemantikus fája.

BIZONYÍTÁS.

  1. Tegyük fel, hogy S kielégíthetetlen. Legyen T az S egy Herbrand-bázisához tartozó teljes szemantikus fa. A T szemantikus fa minden ága egy-egy Herbrand-interpretációt határoz meg. T minden ágán van legalább egy cáfoló csúcs, mert különben az ágnak megfelelő interpretáció kielégítené S Herbrand-univerzum feletti alapklózainak halmazát, azaz az S klózhalmazt is. Zárjuk le az ágakat a gyökérhez legközelebbi cáfoló csúcsokkal. Ez azt jelenti, hogy az egyes ágakra S egy-egy klózának egy-egy alappéldányát illesztjük. Mivel a klózok véges sok literált tartalmaznak, ezek a cáfoló csúcsok a gyökértől mind véges távolságra vannak. Tehát S-nek van véges zárt szemantikus fája.

  2. Tegyük most fel, hogy S-nek van véges zárt szemantikus fája, legyen ez például a T. A T minden ága tartalmaz cáfoló csúcsot. Ez viszont azt jelenti, hogy minden Herbrand-interpretáció hamissá tesz S legalább egy klózának egy alappéldányát. Tehát S kielégíthetetlen.

Herbrand tételének 1. változatát tehát bebizonyítottuk.

6.3.64. TÉTEL. (HERBRAND TÉTELE, 2. VÁLTOZAT)

Egy S elsőrendű klózhalmaz akkor és csak akkor kielégíthetetlen, ha az S klózai Herbrand-univerzum feletti alappéldányainak van véges kielégíthetetlen S részhalmaza.

BIZONYÍTÁS.

  1. Tegyük fel, hogy S kielégíthetetlen. Legyen T az S egy Herbrand-bázisához tartozó teljes szemantikus fa. A 6.3.63. tétel szerint T-nek van véges zárt szemantikus fája, legyen ez T. Legyen S a T-vel cáfolt alapklózok halmaza. T végessége miatt az S véges és a konstrukció miatt kielégíthetetlen.

  2. Tegyük fel, hogy van az S klózai Herbrand-univerzum feletti alappéldányainak véges kielégíthetetlen S részhalmaza. Mivel S minden interpretációja tartalmazza S egy interpretációját, ha nem elégíti ki S-t, akkor sem elégíti ki S-t. Viszont S kielégíthetetlen, így nem elégítheti ki S-t, tehát nem elégítheti ki S egyetlen interpretációja sem. Emiatt S-t sem elégítheti ki egyetlen interpretációja sem, azaz S kielégíthetetlen.

Így a Herbrand-tétel 2. változata is bizonyítást nyert.

6.3.65. PÉLDA.

  1. Legyen S={P(x),¬P(f(a))}. Az S elsőrendű klózhalmaz kielégíthetetlen, mert S Herbrand-univerzum feletti alapklózainak

{ P ( f ( a ) ) , ¬ P ( f ( a ) ) }

egy véges kielégíthetetlen részhalmaza.

  1. Az S={¬P(x)Q(f(x),x),P(g(b)),¬Q(y,z)} kielégíthetetlen, mert S Herbrand-univerzum feletti alapklózainak

{ ¬ P ( g ( b ) ) Q ( f ( g ( b ) ) , g ( b ) ) , P ( g ( b ) ) , ¬ Q ( f ( g ( b ) ) , g ( b ) ) }

egy véges kielégíthetetlen részhalmaza. Ezek az alapklózok az xg(b), yf(g(b)), zg(b) változókiértékelés mellett álltak elő. Legyen a Herbrand-univerzum elemsorrendje

b , f ( b ) , g ( b ) , f ( g ( b ) ) , g ( f ( b ) ) , f ( f ( b ) ) , .

Az alapklózok szisztematikus előállítása során a

¬ P ( g ( b ) ) Q ( f ( g ( b ) ) , g ( b ) )

alapklóz ekkor a nyolcadikként, a ¬Q(f(g(b)),g(b)) pedig huszonkettedikként áll elő.

Davis és Putnam módszere

A Herbrand-tételeket felhasználó, az alapklózok halmazának kielégíthetetlenségének kérdését megválaszoló eljárások közül az első 1960-ban Davis és Putnam módszere, egy későbbi pedig az alaprezolúció Herbrand-univerzumon.

Legyen S alapklózok egy halmaza. A Davis–Putnam-módszer négy szabály alkalmazásával csökkenti S elemeinek számát. Ha S kielégíthető, akkor minden klóz törlődik. Ha S kielégíthetetlen, akkor az üres klóz bekerül a klózhalmazba.

  1. Tautológia szabály (Tautology Rule): Egy klózt nevezzünk tautológiának, ha tartalmaz komplemens literálpárt. Törölni kell S-ből minden tautológiát. Ha a megmaradó S alapklózhalmaz üres, akkor megállunk, egyébként a megmaradó S alapklózhalmazzal folytatjuk az eljárást.

  2. Egy-literál szabály (One-Literal Rule): Ha S-ben van egy L egységalapklóz, akkor S-ből úgy kapjuk S-t, hogy S-ből elhagyjuk az L-et tartalmazó alapklózokat. Ha S üres, akkor megállunk, egyébként előállítjuk S-t az S-ből úgy, hogy töröljük ¬L-et az S alapklózaiból. Megjegyezzük, hogy ha S-ben volt ¬L egységklóz, akkor ez a klóz ¬L törlése után az üres klóz () lesz és ekkor is megállunk. Egyébként az S alapklózhalmazzal folytatjuk az eljárást.

  3. Tiszta-literál szabály (Pure-Literal Rule): Azt mondjuk, hogy S egy alapklózában lévő L literál tisztaS-ben, ha ¬L nem fordul elő S egyetlen klózában sem. Ha L tiszta S-ben, akkor S-ből úgy kapjuk S-t, hogy S-ből elhagyunk minden L -et tartalmazó alapklózt. A megmaradó S alapklózhalmazzal, ha az nem üres, folytatjuk az eljárást.

  4. Szétvágási szabály (Splitting Rule): Ez a szabály akkor alkalmazható, ha S klózai a következőképpen csoportosíthatók:

{ ( A 1 L ) , ( A 2 L ) , , ( A m L ) } , { ( B 1 ¬ L ) , ( B 2 ¬ L ) , , ( B n ¬ L ) } , R ,

ahol R={R1,R2,,Rs}, és az Ai,Bi,Ri alapklózok nem tartalmazzák sem L -et, sem ¬L-et. Legyen ekkor S1={A1,A2,,Am}R és S2={B1,B2,,Bn}R. A kapott S1 és S2 klózhalmazokkal dolgozunk tovább.

Egy új kalkulus alkalmazhatóságának alapfeltétele az eljárás helyessége és teljessége. Esetünkben elég a következő tételt belátni:

6.3.66. TÉTEL. Egy S alapklózhalmaz akkor és csak akkor kielégíthetetlen, ha a Davis–Putnam-módszer szabályainak alkalmazásával S-ből kapott alapklózhalmaz(ok) kielégíthetetlen(ek).

BIZONYÍTÁS.

  1. Mivel a tautológiákat minden interpretáció kielégíti, az S alapklózhalmaz valóban pontosan akkor kielégíthetetlen, ha S kielégíthetetlen.

  2. Ha S üres, akkor minden S-beli alapklóz tartalmazza az S-beli L egységalapklózt, így minden olyan interpretáció, amelyben L igaz, kielégíti S-t. Következésképpen S kielégíthető.

    Most megmutatjuk, hogy az S alapklózhalmaz akkor és csak akkor kielégíthetetlen, ha S kielégíthetetlen.

    1. Tegyük fel, hogy S kielégíthetetlen. Ha S kielégíthető lenne, akkor lenne S-t kielégítő interpretáció. -ben L biztosan igaz, mivel L egységalapklóz S-ben. Az továbbá kielégíti az S klózhalmaz minden, L-et nem tartalmazó klózát is. Mivel azonban -ben ¬L hamis, így biztosan kielégíti a ¬L-et tartalmazó alapklózokat a ¬L törlése után is, így kielégíti S-t. Ez ellentmond annak a feltételezésnek, hogy S kielégíthetetlen.

    2. A másik irányt vizsgálva tegyük fel, hogy S kielégíthetetlen. Ha S kielégíthető lenne, akkor lenne S-t kielégítő interpretáció. Mivel L és ¬L egyike sem szerepel S-ben, választható úgy, hogy benne L igaz. Ez az kielégíti S-t. De ez ellentmond annak a feltételezésnek, hogy S kielégíthetetlen.

3. S akkor és csak akkor kielégíthetetlen, ha S kielégíthetetlen.

  1. Tegyük fel, hogy S kielégíthetetlen. Ekkor S biztosan kielégíthetetlen, mivel S'S.

  2. Most fordítva: tegyük fel, hogy S kielégíthetetlen. Ha S kielégíthető lenne, akkor lenne S-t kielégítő interpretáció. Mivel S-ben nem fordul elő sem L, sem ¬L, ezért -ben L igazságértéke tetszőleges. Válasszuk azt az interpretációt, ahol L igazságértéke i. De S-nek egy ilyen interpretációja kielégíti S-t is. Ez pedig ellentmond annak, hogy S kielégíthetetlen.

4. S akkor és csak akkor kielégíthetetlen, ha mind S1, mind S2 kielégíthetetlen.

  1. Tegyük fel, hogy S kielégíthetetlen. Ha S1 és S2 valamelyike kielégíthető lenne, akkor lenne vagy S1-et, vagy S2-t kielégítő interpretáció. Mivel S1 (S2) egyikében sem fordul elő L és ¬L egyike sem, ezért az interpretációban L igazságértéke tetszőleges. Ha az S1-et kielégítő interpretáció, válasszuk úgy, hogy benne L hamis, illetve ha az S2-t kielégítő interpretáció, válasszuk úgy, hogy benne L igaz legyen. Bármelyik kielégíti S-t. Ez ellentmond annak, hogy S kielégíthetetlen. Tehát mind S1, mind S2 kielégíthetetlen.

  2. A másik irányt vizsgálva kiindulunk abból, hogy mind S1, mind S2 kielégíthetetlen. Ha S kielégíthető lenne, akkor lenne S-t kielégítő interpretáció. Ha -ben ¬L (L) igazságértéke i, akkor kielégítené S1-et (S2-t). Ez ellentmondásban van azzal, hogy mind S1, mind S2 kielégíthetetlen. Így S-nek kielégíthetetlennek kell lennie.

Ezzel a tételt bebizonyítottuk.

Most néhány példán keresztül bemutatjuk a Davis–Putnam-módszer alkalmazását.

6.3.67. PÉLDA.

  1. Alkalmazzuk a módszert az S={XY¬Z,X¬Y,¬X,Z,U} klózhalmazra.

S = { Y ¬ Z , ¬ Y , Z , U }

[ 2. szabály ¬X-szel ]

S = { ¬ Z , Z , U }

[ 2. szabály ¬Y-nal ]

S = { , U }

[ 2. szabály ¬Z-vel ]

S kielégíthetetlen, mivel S már tartalmazza az üres klózt.

  1. Vizsgáljuk az S={XY,¬Y,¬XY¬Z} klózhalmazt.

S = { X , ¬ X ¬ Z }

[ 2. szabály ¬Y-nal ]

S = { ¬ Z }

[ 2. szabály X-szel ]

S = { }

[ 2. szabály ¬Z-vel ]

S kielégíthető, mivel S üres.

  1. Legyen S={X¬Y,¬XY,Y¬Z,¬Y¬Z}.

S 1 = { ¬ Y , Y ¬ Z , ¬ Y ¬ Z } , S 2 = { Y , Y ¬ Z , ¬ Y ¬ Z }

[ 4. szabály X-szel ]

S 1 = { ¬ Z } , S 2 = { ¬ Z }

[ 2. szabály Y-nal és ¬Y-nal ]

S 1 = { } , S 2 = { }

[ 2. szabály ¬Z-vel ]

Mivel mind S1, mind S2 kielégíthető, S is kielégíthető.

  1. Ha S={X¬Y,XY,YZ,¬YZ}, akkor:

S = { Y Z , ¬ Y Z }

[ 3. szabály X-szel ]

S = { }

[ 3. szabály Z-vel ]

Tehát S kielégíthető.

Megjegyezzük, hogy a Davis-Putnam-módszer szabályai nagyon fontosak a rezolúciós stratégiák tulajdonságainak vizsgálatában is ([15]). A fejezet elején említett másik módszer a Herbrand-univerzum feletti alaprezolúció. A 6.3.65. példa (b) része mutatja, hogy az alaprezolúció hatékonysága elég gyenge. Az alaprezolúció azonban mégis nagy jelentőségű az elsőrendű rezolúció kialakulása szempontjából ([20]).

A Herbrand-univerzum feletti alaprezolúcióhoz egy elsőrendű klóz magjában az individuumváltozókat Herbrand-univerzumbeli elemekkel helyettesítjük. Az alaprezolúció már ismert, de az univerzum egyedisége miatt mégis mutatunk a módszerre néhány példát.

6.3.68. PÉLDA.

  1. Legyen az elsőrendű klózhalmaz S={P(x),¬Q(y,z)¬P(z),Q(u,v)}. Ekkor ={a}. A Herbrand-bázis: {P(a),Q(a,a)}. Az alapklózhalmaz: S={P(a),¬Q(a,a)¬P(a),Q(a,a)}.

Egy alaprezolúciós levezetés:

1.

P ( a )

[ S ]

2.

¬ Q ( a , a ) ¬ P ( a )

[ S ]

3.

¬ Q ( a , a )

[ 1, 2 rezolvense ]

4.

Q ( a , a )

[ S ]

5.

[ 3, 4 rezolvense ]

  1. Tekintsük az S={P(x),¬Q(y,z)¬P(z),Q(u,f(u))} klózhalmazt.

A Herbrand-univerzum:

0

=

{ a } extra szimbólum

1

=

{ a , f ( a ) }

2

=

{ a , f ( a ) , f ( f ( a ) ) }

=

{ a , f ( a ) , f ( f ( a ) ) , f ( f ( f ( a ) ) ) ,... }

A Herbrand-bázis:

{ P ( a ) , Q ( a , a ) , P ( f ( a ) ) , Q ( a , f ( a ) ) , Q ( f ( a ) , a ) , Q ( f ( a ) , f ( a ) ) , P ( f ( f ( a ) ) ) , }

Legyen egy változókiértékelés: xf(a), ya, zf(a), ua.

A kapott alapklózhalmaz:

S = { P ( f ( a ) ) , ¬ Q ( a , f ( a ) ) ¬ P ( f ( a ) ) , Q ( a , f ( a ) ) } .

Egy alaprezolúciós levezetés:

1.

¬ Q ( a , f ( a ) ) ¬ P ( f ( a ) )

[ S ]

2.

Q ( a , f ( a ) )

[ S ]

3.

¬ P ( f ( a ) )

[ 1, 2 rezolvense ]

4.

P ( f ( a ) )

[ S ]

5.

[ 3, 4 rezolvense ]

A rezolúciós kalkulus az elsőrendű logikában

A 6.3.4. fejezetben elsőrendű literálnak neveztük az atomi formulákat és az atomi formulák negáltjait. Egy elsőrendű literál alapja a literálban szereplő atomi formula volt, és ha két literálban az atomi formula ugyanaz, azonos alapú literáloknak neveztük őket. Komplemens literálpár két azonos alapú literál, ha az egyikben az alap negáltan, a másikban negálatlanul szerepel. Tegyük most fel, hogy két elsőrendű klózban pontosan egy komplemens literálpár fordul elő. Nulladrendű klózok esetén ekkor előállíthattuk a klózok speciális alakú következményét: rezolvensüket. Feltesszük a kérdést, hogy a rezolvenst előállíthatnánk-e elsőrendű klózok esetén is:

6.3.69. PÉLDA. Legyen két elsőrendű klóz

C 1 = x ( P ( f ( x ) ) Q ( x ) ) és C 2 = x y ( ¬ P ( f ( x ) ) R ( x , y ) ) .

C 1 és C2 pontosan egy komplemens literálpárt tartalmaz. Ha a magjaikból a nulladrendű esethez hasonlóan képezzük a rezolvenst, a

C = x y ( Q ( x ) R ( x , y ) )

klózhoz jutunk. Lássuk be, hogy {C1,C2}C, azaz

{ x ( P ( f ( x ) ) Q ( x ) ) , x y ( ¬ P ( f ( x ) ) R ( x , y ) ) } x y ( Q ( x ) R ( x , y ) ) .

Ahhoz, hogy egy interpretáció kielégítse C1 és C2 klózokat, a P(f(x))Q(x) és ¬P(f(x))R(x,y) formulák igazságértéke minden változókiértékelés mellett i kell legyen -ben. Ez csak úgy lehet, hogy azokra a κ változókiértékelésekre, amelyekre |P(f(x))|,κ=h, a |Q(x)|,κ=i, és azokra, ahol |¬P(f(x))|,κ=h, az |R(x,y)|,κ=i. Mivel minden κ-ra |P(f(x))|,κ=i esetén |¬P(f(x))|,κ=h és fordítva, vagy a |Q(x)|,κ=i, vagy az |R(x,y)|,κ=i fennáll, és így |xy(Q(x)R(x,y))|,κ=i.

Ha ilyen módon képezve elsőrendű klózok rezolvensét szeretnénk ezt rezolúciós levezetési szabályként alkalmazni, akkor igazolni kell általánosan is a példabeli állítást.

6.3.70. TÉTEL. Legyenek most C1 és C2 olyan elsőrendű klózok, melyek pontosan egy komplemens literálpárt tartalmaznak, azaz C1 és C2 magjai C1M=C1ML1 és C2M=C2ML2 alakúak, ahol L1 és L2 komplemens literálpár. Ha CM=C1MC2M a C klóz magja, akkor {C1,C2}C.

BIZONYÍTÁS. Tegyük fel hogy az interpretáció kielégíti a {C1,C2} elsőrendű klózhalmazt. Kövessük a 6.3.69. példabeli gondolatmenetet. Az interpretációban tetszőleges κ változókiértékelés mellett vagy L1 és C2M, vagy L2 és C1Migaz. Azaz -ben C igaz.

Az alábbi példában látjuk majd, hogy komplemens párt látszólag nem tartalmazó két elsőrendű klóz Herbrand-univerzum feletti alappéldányai között lehetnek olyanok, amelyekben találunk komplemens párt.

6.3.71. PÉLDA. Legyen a változóiban tiszta klózhalmaz:

{ x y ( P ( x ) ¬ Q ( x , f ( y ) ) ) , z v ( ¬ P ( g ( z ) ) ¬ P ( v ) ) , u Q ( g ( u ) , u ) } .

Látjuk, hogy egyik klózpárban sincs komplemens literálpár. Alaprezolúcióval vizsgáljuk meg, hogy a klózhalmaz kielégíthetetlen-e. A Herbrand-univerzum:

{ a , g ( a ) , f ( a ) , g ( f ( a ) ) , g ( g ( a ) ) , f ( f ( a ) ) , f ( g ( a ) ) , } .

Állítsunk elő a Herbrand-univerzum felett néhány alappéldányát

  • a xy(P(x)¬Q(x,f(y))) klóznak:

x

y

P ( x ) ¬ Q ( x , f ( y ) )

a

a

P ( a ) ¬ Q ( a , f ( a ) )

g ( a )

a

P ( g ( a ) ) ¬ Q ( g ( a ) , f ( a ) )

a

g ( a )

P ( a ) ¬ Q ( a , f ( g ( a ) ) )

g ( f ( a ) )

a

P ( g ( f ( a ) ) ) ¬ Q ( g ( f ( a ) ) , f ( a ) )

  • a zv(¬P(g(z))¬P(v)) klóznak:

z

v

¬ P ( g ( z ) ) ¬ P ( v )

a

a

¬ P ( g ( a ) ) ¬ P ( a )

a

g ( a )

¬ P ( g ( a ) ) ¬ P ( g ( a ) )

f ( a )

g ( a )

¬ P ( g ( f ( a ) ) ) ¬ P ( g ( a ) )

f ( a )

g ( f ( a ) )

¬ P ( g ( f ( a ) ) ) ¬ P ( g ( f ( a ) ) )

  • a uQ(g(u),u) klóznak:

u

Q ( g ( u ) , u )

a

f ( a )

Q ( g ( a ) , a )

Q ( g ( f ( a ) ) , f ( a ) )

Egy alaprezolúciós levezetés:

1.

Q ( g ( f ( a ) ) , f ( a ) )

[ u f ( a ) ]

2.

P ( g ( f ( a ) ) ) ¬ Q ( g ( f ( a ) ) , f ( a ) )

[ x g ( f ( a ) ) , y a ]

3.

P ( g ( f ( a ) ) )

4.

¬ P ( g ( f ( a ) ) )

[ z f ( a ) , v g ( f ( a ) ) ]

5.

Megfigyelhetjük, hogy a levezetéshez az alapklózok közül ki lehetett választani olyan klózpárokat, amelyekben komplemens literálpárok szerepeltek, így a rezolúciós levezetést elő tudtuk állítani. Tegyünk egy új változót a kiválasztott alapklózokban az a helyébe. Ekkor a következő rezolúciós levezetés már elsőrendű klózokból való levezetés lesz:

1.

Q ( g ( f ( w ) ) , f ( w ) )

[ ( u f ( w ) ) ]

2.

P ( g ( f ( w ) ) ) ¬ Q ( g ( f ( w ) ) , f ( w ) )

[ ( x , y g ( f ( w ) ) , w ) ]

3.

P ( g ( f ( w ) ) )

4.

¬ P ( g ( f ( w ) ) )

[ ( z , v f ( w ) , g ( f ( w ) ) ) ]

5.

Ez a levezetés a

{ w ( P ( g ( f ( w ) ) ) ¬ Q ( g ( f ( w ) ) , f ( w ) ) ) , w ¬ P ( g ( f ( w ) ) ) , w Q ( g ( f ( w ) ) , f ( w ) ) }

klózhalmazból való egy rezolúciós levezetés. Ezt a klózhalmazt úgy kaptuk az eredetiből, hogy az elsőrendű klózok magjaiban az atomi formulákban az individuumváltozók helyébe olyan termeket helyettesítettünk, amelyek azonos alapú literálokat eredményeztek. Ezzel a – logikában egyébként nem megengedett – helyettesítéssel a klózhalmaz kielégíthetősége megőrződik, viszont a kapott elsőrendű klózhalmaz alappéldányai csak olyanok lesznek, amelyekben a lehetséges komplemens párok megjelennek. Úgy is fogalmazhatunk, hogy ily módon kiszűrjük azokat az alapklózokat, amelyek egy alaprezolúciós levezetésbe biztosan nem kerülnének be.

6.3.72. TÉTEL. Legyen CM a C</