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.

Chapter 7. Alkalmazások

Chapter 7. Alkalmazások

Formalizálás – problémamegoldás

A formális axiomatikus elméletekről

Láttuk, hogy egy elsőrendű logikai nyelv interpretációja tetszőleges – valamely U univerzumon értelmezett – a nyelvvel megegyező szignatúrájú (típusú) matematikai struktúra lehet. Egy matematikai struktúra vagy struktúraosztály axiomatizálása a megfelelő elsőrendű nyelven leírt olyan zárt formulák halmazának megadása, amelyek igazak az illető struktúrában, és felhasználásukkal, valamint a logika valamelyik tételbizonyító kalkulusának alkalmazásával minden a struktúra(osztályban) igaz formula levezethető. Az említett (axióma)formulák tulajdonképpen a struktúra(osztály) műveleteinek és relációinak tulajdonságait és azok egymáshoz való viszonyát írják le. A modellelmélet a matematikai logikának az az ága, amely a matematikai struktúrák axiomatizálási kérdéseivel és adott axiómarendszerekhez azokat kielégítő struktúrák (modellek) osztályaival foglalkozik. Az első modellelméleti eredmények az 1930-as években születtek (Löwenheim, Skolem, Herbrand), az első összefoglaló mű pedig 1973-ban jelent meg [14].

7.1.1. DEFINÍCIÓ. Formális axiomatikus elmélet alatt egy T=,A párt értünk, ahol elsőrendű logikai nyelv és A zárt formuláinak egy halmaza. A formuláit a T elmélet logikán kívüli axiómáinak nevezzük.

7.1.2. DEFINÍCIÓ. Az elsőrendű logikai nyelv egy interpretációja a T=,A (formális axiomatikus) elmélet modellje, ha minden AA formulára |A|=i.

Egy elmélet modellje tehát, ha egyáltalán van, egy általános matematikai struktúra. Egy matematikai struktúrát pedig, ha hangsúlyozni kívánjuk, hogy modellje valamely elméletnek, axiomatizált struktúrának nevezünk.

Most felsorolunk néhány ismert elméletet, megadva az elmélet logikán kívüli axiómáit. Ezen elméletek leíró nyelvei egyenlőségjeles nyelvek, ezért a logikai axiómákhoz hozzá kell venni – a nyelv ábécéjére szabottan – az egyenlőség axiómáit is. Ezek közül az

  1. x ( x = x )

  2. x y ( x = y y = x )

  3. x y z ( x = y y = z x = z )

axiómák minden nyelvben ugyanazok.

A hálók

nyelve: =;,;(2;2,2;0) szignatúrával

axiómarendszere:

  1. x y ( x y = y x )

  2. x y ( x y = y x )

  3. x y z ( ( x y ) z = x ( y z ) )

  4. x y z ( ( x y ) z = x ( y z ) )

  5. x y ( x ( x y ) = x )

  6. x y ( x ( x y ) = x )

az egyenlőség axiómái a nyelv ábécéjére szabottan:

  1. x y z v ( x = z y = v x y = z v )

  2. x y z v ( x = z y = v x y = z v )

A rendezett halmazok

nyelve: =,R;;(2,2;;0) szignatúrával

axiómarendszere:

  1. x ¬ R ( x , x )

  2. x y z ( R ( x , y ) R ( y , z ) R ( x , z ) )

  3. x y ( R ( x , y ) R ( y , x ) x = y )

az egyenlőség axiómái a nyelv ábécéjére szabottan:

  1. x y z v ( x = y z = v R ( x , y ) R ( z , v ) )

A csoportelmélet

nyelve: =;;e(2;2;1) szignatúrával

axiómarendszere:

  1. x y z ( x ( y z ) = ( x y ) z )

asszociativitás

  1. x ( x e = x e x = x )

egységelem

  1. x y ( x y = e y x = e )

inverz

az egyenlőség axiómái a nyelv ábécéjére szabottan:

  1. x y z v ( x = z y = v x y = z v )

Az elemi aritmetika

nyelve: az Ar nyelv

axiómarendszere (Peano-axiómarendszer):

  1. x ( s ( x ) 0 )

  1. x y ( s ( x ) = s ( y ) x = y )

indukció (másodrendű nyelven formalizálható)

  1. A ( A ( 0 ) x ( A ( x ) A ( s ( x ) ) ) x A ( x )

műveletdefiníciók

  1. x ( x + 0 = x )

  1. x y ( x + s ( y ) = s ( x + y ) )

  1. x ( x 0 = x )

  1. x y ( x s ( y ) = x y + x )

az egyenlőség axiómái a nyelv ábécéjére szabottan:

  1. x y z v ( x = z y = v x + y = z + v )

  1. x y z v ( x = z y = v x y = z v )

  1. x y ( x = y s ( x ) = s ( y ) )

Legyen adott egy T elmélet és egy tételbizonyítási feladat (feltételeknek egy Γ halmaza és egy B tételformula). A tétel bizonyítására válasszuk ki valamelyik tételbizonyító eljárást (kalkulust). Nem szorul magyarázatra, hogy a következtetés során a T elmélet logikán kívüli axiómáit a Γ-beli formulákon túl mint feltételformulákat fogjuk felhasználni.

7.1.3. DEFINÍCIÓ. Azt mondjuk, hogy az nyelv egy B formulája az A formulahalmazzal megadott Telmélet tétele, ha valamely (bármely) helyes és teljes tételbizonyító kalkulussal A-ból levezethető B (ez pontosan azt jelenti, hogy AB). A B az elméletnek valamely Γfeltételhalmaz mellett tétele, ha B levezethető AΓ-ból (ekkor AΓB).

7.1.4. DEFINÍCIÓ. Egy elmélet ellentmondásmentes, ha annak nincs olyan zárt B formulája, hogy B is, és ¬B is az elmélet tétele lenne. Egy elmélet teljes, ha annak bármely zárt B formulája esetén vagy B, vagy ¬B az elmélet tétele.

Az axiomatizálás lehetőségeinek korlátait mutatja meg Gödel nemteljességi tétele. A tétel egy megfogalmazása: ,,Az elemi aritmetika (az Ar nyelv a Peano-axiómarendszerrel) ellentmondásmentes, ugyanakkor nem teljes. Ugyanis a természetes számok szokásos struktúrájával modellezve az elemi aritmetika elméletét, van olyan zárt formula, amely igaz e modellben, de sem a formula, sem a negáltja nem tétele az elméletnek.” Sőt, ez nemcsak az elemi aritmetikára (Peano-axiómarendszerre) igaz, hanem a természetes számok bármely ,,elég erős” elméletére is.

7.1.5. PÉLDA. Legyen a T elmélet a csoportelmélet. Bizonyítsuk be az egyszerű

x y z ( x y = e z x = e y = z )

tételt. Jelölje a tételt B.

  1. A csoportelmélet (1)(3), az egyenlőség (1) axiómáiból és ¬B-ből állítsunk elő elsőrendű klózhalmazt. Ehhez egyrészt a (3) axiómából az f Skolem-függvény bevezetésével, másrészt a

¬ B x y z ( x y = e z x = e ¬ ( y = z ) )

formulából az a Skolem-konstans bevezetésével elimináljuk az egzisztenciális kvantort. Az S változóiban tiszta elsőrendű klózhalmaz klózai a következők:

  1. x 1 ( y 1 z 1 ) = ( x 1 y 1 ) z 1

  1. x 2 e = x 2

  1. e x 3 = x 3

  1. x 4 f ( x 4 ) = e

  1. f ( x 5 ) x 5 = e

  1. a y 2 = e

  1. z 1 a = e

  1. ¬ ( y = z )

  1. x = x

Az elsőrendű rezolúciós levezetés:

  1. ¬ ( y = z )

[ S ]

  1. x = x

[ S ]

[ 1, 2 rezolvense (y,zx,x) mellett ]

  1. Ha alaprezolúcióval dolgoznánk, akkor a Herbrand-univerzum:

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

Az xa,ya,za változókiértékelés mellett 8.-ból a ¬(a=a), 9.-ből az a=a egységklózokat kapjuk. Ezekből az alapklózokból egyetlen rezolúciós lépésben megkapjuk az üres klózt.

  1. Bizonyítsuk be a tételt tablómódszerrel. Állítsuk elő az 1–9. formulák és a ¬B tablóját. Először ¬B befejezett tablóját állítjuk elő, majd folytatva a x(x=x) axiómaformulával a tabló zárttá válik:

¬ x y z ( x y = e z x = e y = z )

¬ y z ( a y = e z a = e y = z )

[ 1-ből, a kritikus paraméter ]

¬ z ( a a = e z a = e a = z )

[ 2-ből ]

¬ ( a a = e a a = e a = a )

[ 3-ból ]

( a a = e a a = e )

[ 4-ből A szabály ]

¬ ( a = a )

[ 4-ből A szabály ]

x ( x = x )

[ (4) axióma ]

( a = a )

[ 7-ből D szabály ]

×

[ 6, 8 miatt ]

7.1.6. PÉLDA. Most bebizonyítjuk, hogy az egyenlőség

(1)

x ( x = x )

(2)

x y ( x = y y = x )

(3)

x y z ( x = y y = z x = z )

logikai axiómarendszerével egyenértékű az

( 1 )

x ( x = x )

( 2 )

x y z ( x = y x = z y = z )

formulahalmaz, azaz {(1),(2),(3)}(1) és {(1),(2),(3)}(2), továbbá {(1),(2)}(1), {(1),(2)}(2) és {(1),(2)}(3). Ez azt jelenti, hogy {(1),(2)} is használható az egyenlőség logikai axiómarendszereként. Mivel (1) és (1) megegyeznek, elég az alábbiakat igazolni:

  1. Bebizonyítjuk rezolúciós kalkulussal, hogy a {(2),(3),¬(2)} formulahalmaz kielégíthetetlen. A kalkulus alkalmazásához előállítjuk a megfelelő klózhalmazt:

formula

klóz(ok)

x y ( x = y y = x )

¬ ( x 1 = y 1 ) y 1 = x 1

x y z ( x = y y = z x = z )

¬ ( x 2 = y 2 ) ¬ ( y 2 = z 2 ) x 2 = z 2

¬ x y z ( x = y x = z y = z )

a = b , a = c , ¬ ( b = c )

Tehát az

S = { ¬ ( x 1 = y 1 ) y 1 = x 1 , ¬ ( x 2 = y 2 ) ¬ ( y 2 = z 2 ) x 2 = z 2 , a = b , a = c , ¬ ( b = c ) }

klózhalmaz kielégíthetetlenségét kell igazolnunk. A rezolúciós levezetés:

  1. ¬ ( x 1 = y 1 ) y 1 = x 1

[ S ]

  1. a = b

[ S ]

  1. b = a

[ 1, 2 rezolvense (x1,y1a,b) mellett ]

  1. ¬ ( x 2 = y 2 ) ¬ ( y 2 = z 2 ) x 2 = z 2

[ S ]

  1. ¬ ( a = z 2 ) b = z 2

[ 3, 4 rezolvense (x2,y2b,a) mellett ]

  1. a = c

[ S ]

  1. b = c

[ 5, 6 rezolvense (z2c) mellett ]

  1. ¬ ( b = c )

[ S ]

[ 7, 8 rezolvense ]

2. Bebizonyítjuk természetes technikával, hogy (1),(2)(2). Felhasználva kétszer egymás után az univerzális kvantor bevezetésének szabályát, elég az (1),(2)x=yy=x szekvenciát megalapozni. Az implikáció bevezetését alkalmazva az (1),(2),x=yy=x, majd az implikáció alkalmazásának szabályával az

( 1 ) , ( 2 ) , x = y x = y x = x

és az

( 1 ) , ( 2 ) , x = y x = y x = x y = x

szekvenciák igazolására vezethetjük vissza a feladatot. Az első szekvencia megalapozásához alkalmazzuk a konjunkció bevezetésének szabályát, így az

( 1 ) , ( 2 ) , x = y x = y és az ( 1 ) , ( 2 ) , x = y x = x

szekvenciákat nyerjük, melyek egyike az azonosság törvénye, a másik pedig az univerzális kvantor alkalmazása után lesz az, mivel (1) hipotézis. A második szekvenciát pedig az univerzális kvantor alkalmazása szabályának háromszori alkalmazása után nyert

( 1 ) , ( 2 ) , x = y x y z ( x = y x = z y = z )

azonosság törvénye igazolja (hiszen épp a (2) hipotézis a levezetendő formula).

3. Az előző bizonyítást felhasználva azt is igazolhatjuk, hogy (1),(2)(3). A vágás szabályának alkalmazásával ugyanis az

( 1 ) , ( 2 ) ( 2 ) és a ( 2 ) , ( 2 ) ( 3 )

szekvenciák megalapozására vezetjük vissza a bizonyítást. Az első szekvenciát az előbb igazoltuk. A (2),(2)(3) szekvencia bizonyításához alkalmazzuk az univerzális kvantor bevezetésének szabályát:

( 2 ) , ( 2 ) x = y y = z x = z .

Az implikáció bevezetésének, majd a konjunkció alkalmazásának szabályai segítségével a

( 2 ) , ( 2 ) , x = y , y = z x = z

megalapozandó szekvenciához jutunk. Vezessük most vissza a feladatot az implikáció alkalmazásának szabályával a

( 2 ) , ( 2 ) , x = y , y = z y = x y = z

és a

( 2 ) , ( 2 ) , x = y , y = z y = x y = z x = z

szekvenciák igazolására. Az első szekvencia megalapozásához alkalmazzuk a konjunkció bevezetésének szabályát, így a

( 2 ) , ( 2 ) , x = y , y = z y = x és a ( 2 ) , ( 2 ) , x = y , y = z y = z

szekvenciákat nyerjük. A jobb oldali szekvencia az azonosság törvénye, a bal oldali szekvencia igazolásához pedig újból alkalmazzuk az implikáció alkalmazásának a szabályát; az igazolandó szekvenciák:

( 2 ) , ( 2 ) , x = y , y = z x = y

és

( 2 ) , ( 2 ) , x = y , y = z x = y y = x .

Az egyik nyert szekvencia az azonosság törvénye, a másik pedig az univerzális kvantor alkalmazása után a (2) hipotézis miatt lesz az. A

( 2 ) , ( 2 ) , x = y , y = z y = x y = z x = z

szekvencia pedig ugyancsak az univerzális kvantor alkalmazásával igazolható a (2) hipotézis segítségével.

A formalizálás kérdései

Egy matematikai probléma mindig egy adott struktúrával (vagy struktúraosztállyal) kapcsolatban merül fel. A probléma formalizálásához pedig az illető struktúra(osztály) leíró nyelvének használata célszerű. Mint láttuk, egy adott matematikai probléma szintaktikai eszközökkel való megoldása feltételezte a struktúra(osztály) axiomatizálását. Ezért a formalizáláshoz hozzátartozik az elmélet leíró formuláinak megadása is. Ezután a probléma mint tételbizonyítási feladat, bármelyik teljes tételbizonyító kalkulussal megoldható.

Ha egy adott, nem matematikai probléma megoldásában logikai eszközökkel szeretnénk dolgozni, akkor a problémát és minden körülményt, amely ok-okozati kapcsolatba hozható a problémával, egy formális rendszerbeli környezetbe kell elhelyezni. Ehhez rögzíteni kell a probléma megoldásához szükséges nyelvi elemeket, vagyis azokat a reláció- és függvényszimbólumokat, melyekkel ki lehet fejezni a probléma kapcsán érintett objektumok közötti kapcsolatokat. Ezek mellett, illusztrációként, megadhatunk egy a nyelvnek megfelelő struktúrát (modellt) is, amely a nyelv logikán kívüli jeleinek szándékolt jelentését rögzíti. Az így kialakított elsőrendű nyelven formalizáljuk a problémát és a probléma környezetében meglévő speciális kapcsolatrendszert (axiómarendszer), valamint a feltételeket. Ezt a folyamatot nevezzük formalizálásnak.

Az axiómarendszerről (és a feltételhalmazról) mindenképpen be kell látni, hogy ellentmondásmentes. Ehhez hasznos lehet a szándékolt jelentést illusztráló modell. Az axiómarendszerrel kapcsolatos egyéb elvárások, mint például a függetlenség biztosítása, nem feltétlenül szükséges.

A fentiekből látszik, hogy a formalizálás, modellalkotás egy sor önkényes döntés eredménye. Ennek megfelelően egy problémának sok különböző ,,helyes formalizálása” lehet attól függően, hogy a formalizált változattal kapcsolatban milyen további elvárásaink vannak. Például a reláció- és függvényszimbólumok számának optimalizálása, a függvényszimbólumok kizárása, az axiómák számának csökkentése. A ,,jó formalizálás” megtalálása kreatív feladat, amely nem algoritmizálható.

Az alábbiakban egy-egy példán mutatjuk meg kifejezetten nem matematikai problémák formalizálását.

7.1.7. PÉLDA. Kövessük végig a formalizálási folyamatot egy a mesterséges intelligenciában klasszikusnak számító feladaton, a ,,majom és a banán” problémán keresztül. A szakirodalomban e probléma formalizálására több változat is ismert. Most ezek közül mutatunk be egyet.

A szituáció: A szobában van egy majom, egy karosszék, és a mennyezetre fel van függesztve egy köteg banán. A majom a padlóról nem éri el a banánt, de ügyes, a karosszéket tudja mozgatni és fel tud rá mászni. A karosszék elég magas ahhoz, hogy ha éppen a banán alatt van, és a majom a karosszéken áll, akkor a majom elérheti a banánt.

A kérdés: Eléri-e a majom a banánt?

Tehát a szituáció és a kérdés ismeretében megadunk egy alkalmas elsőrendű nyelvet a probléma leírására. A nyelvben a probléma egy tételbizonyítási feladat lesz.

A formalizálás:

  • A szándékolt jelentést megadó struktúra univerzuma a szobában lévő, a megoldás szempontjából fontos objektumok halmaza. Jelölje m a majmot, b a banánt, k a karosszéket, p a padlót. Ekkor U={m,b,k,p}. Legyen a struktúra U;R,M,Z,O,A,T,I,V,F, melynek szignatúrája (2,1,2,2,2,1,1,3,2). A relációk rendre a következők:

R ( x , y )

x eléri y-t

M ( x )

x ügyes

Z ( x , y )

x közvetlenül y közelében van

O ( x , y )

x rajta van y-on

A ( x , y )

x éppen y alatt van

T ( x )

x magas

I ( x )

x a szobában van

V ( x , y , z )

x y -t a z közvetlen közelébe viszi

F ( x , y )

x felmászik y-ra

  • Az A axiómarendszer:

  1. x y ( M ( x ) Z ( x , y ) R ( x , y ) )

  1. x y ( O ( x , y ) A ( y , b ) T ( y ) Z ( x , b ) )

  1. x y z ( I ( x ) I ( y ) I ( z ) V ( x , y , z ) Z ( z , p ) A ( y , z ) )

  1. x y ( F ( x , y ) O ( x , y ) )

Vizsgáljuk meg most ennek az axiómarendszernek az ellentmondásmentességét. Az axiómák Skolem-formulák. Az axiómaformulák magjai olyan implikációk, melyek utótagja három esetben egyetlen atomi formula és egy esetben két atomi formula diszjunkciója. Tehát azok az U feletti interpretációk nyilván kielégítik az axiómaformulákat, ahol az R(x,y), Z(x,b), A(y,z) és O(x,y) relációk a bennük szereplő változók minden kiértékelése mellett igazak. Tehát A ellentmondásmentes.

  • A Γ halmazbeli feltételek:

M ( m )

T ( k )

I ( m ) I ( k ) I ( b )

V ( m , k , b )

¬ Z ( b , p )

F ( m , k )

Vizsgáljuk meg a feltételhalmaz kielégíthetőségét is. Ehhez az kell, hogy legyen olyan interpretáció, melyben rendre |M(m)|=i, |T(k)|=i, |I(m)|=i, |I(k)|=i, |I(b)|=i, |V(m,k,b)|=i, |Z(b,p)|=h és |F(m,k)|=i. Ez nem mond ellent az axiómahalmaz kielégíthetőségi feltételeinek. A feltételhalmazban nem szereplő predikátumszimbólumok és a nem felsorolt változókiértékelések esetén az interpretáció tetszőleges.

Ezután megállapítható, hogy az axiómarendszer kibővítve a feltételformulák halmazával, azaz az (AΓ) formulahalmaz kielégíthető.

  • A B tételformula: R(m,b).

A kérdés megválaszolásához megpróbáljuk belátni, hogy AΓR(m,b). A tétel bizonyításához először az alaprezolúciót, majd pedig a szemantikus fa lezárásának a módszerét alkalmazunk.

  1. A problémamegoldásra alkalmazzuk először a rezolúciós elvet. Ehhez állítsuk elő az axiómaformulákból a változóiban tiszta klózhalmazt:

  A = { ¬ M ( x 1 ) ¬ Z ( x 1 , y 1 ) R ( x 1 , y 1 ) ,           ¬ O ( x 1 , y 1 ) ¬ A ( y 2 , b ) ¬ T ( y 2 ) Z ( x 2 , b ) ,           ¬ I ( x 3 ) ¬ I ( y 3 ) ¬ I ( z 3 ) ¬ V ( x 3 , y 3 , z 3 ) Z ( z 3 , p ) A ( y 3 , z 3 ) ,           ¬ F ( x 4 , y 4 ) O ( x 4 , y 4 ) }

Az R(m,b) tétel bebizonyításához szükséges S=AΓ{¬B} klózhalmaz a következő:

S = { ¬ M ( x 1 ) ¬ ¬ Z ( x 1 , y 1 ) ¬ R ( x 1 , y 1 ) ,          ¬ O ( x 2 , y 2 ) ¬ ¬ A ( y 2 , b ) ¬ ¬ T ( y 2 ) ¬ Z ( x 2 , b ) ,          ¬ I ( x 3 ) ¬ ¬ I ( y 3 ) ¬ ¬ I ( z 3 ) ¬ ¬ V ( x 3 , y 3 , z 3 ) ¬ Z ( z 3 , p ) ¬ A ( y 3 , z 3 ) ,          ¬ F ( x 4 , y 4 ) ¬ O ( x 4 , y 4 ) ,          M ( m ) , T ( k ) , I ( m ) , I ( k ) , I ( b ) ,          V ( m , k , b ) , ¬ Z ( b , p ) , F ( m , k ) ,          ¬ R ( m , b ) }

Végezzük el az

( x 1 , y 1 , x 2 , y 2 , x 3 , y 3 , z 3 , x 4 , y 4 m , b , m , k , m , k , b , m , k )

helyettesítést, ekkor az alábbi alapklózhalmazt kapjuk:

¬ M ( m ) ¬ ¬ Z ( m , b ) ¬ R ( m , b ) , ¬ O ( m , k ) ¬ ¬ A ( k , b ) ¬ ¬ T ( k ) ¬ Z ( m , b ) , ¬ I ( m ) ¬ ¬ I ( k ) ¬ ¬ I ( b ) ¬ ¬ V ( m , k , b ) ¬ Z ( b , p ) ¬ A ( k , b ) , ¬ F ( m , k ) ¬ O ( m , k ) , M ( m ) , T ( k ) , I ( m ) , I ( k ) , I ( b ) , V ( m , k , b ) , ¬ Z ( b , p ) , F ( m , k ) , ¬ R ( m , b ) }

Egy alaprezolúciós levezetés:

1.

¬ R ( m , b )

[ S ]

2.

¬ M ( m ) ¬ Z ( m , b ) R ( m , b )

[ S ]

3.

¬ M ( m ) ¬ Z ( m , b )

[ 1, 2 rezolvense ]

4.

M ( m )

[ S ]

5.

¬ Z ( m , b )

[ 3, 4 rezolvense ]

6.

¬ O ( m , k ) ¬ A ( k , b ) ¬ T ( k ) Z ( m , b )

[ S ]

7.

¬ O ( m , k ) ¬ A ( k , b ) ¬ T ( k )

[ 5, 6 rezolvense ]

8.

¬ F ( m , k ) O ( m , k )

[ S ]

9.

¬ F ( m , k ) ¬ A ( k , b ) ¬ T ( k )

[ 7, 8 rezolvense ]

10.

F ( m , k )

[ S ]

11.

¬ A ( k , b ) ¬ T ( k )

[ 9,10 rezolvense ]

12.

¬ I ( m ) ¬ I ( k ) ¬ I ( b ) ¬ V ( m , k , b ) Z ( b , p ) A ( k , b )

[ S ]

13.

¬ I ( m ) ¬ I ( k ) ¬ I ( b ) ¬ V ( m , k , b ) Z ( b , p ) ¬ T ( k )

[ 11, 12 rezolvense ]

14.

I ( m )

[ S ]

15.

¬ I ( k ) ¬ I ( b ) ¬ V ( m , k , b ) Z ( b , p ) ¬ T ( k )

[ 13, 14 rezolvense ]

16.

I ( k )

[ S ]

17.

¬ I ( b ) ¬ V ( m , k , b ) Z ( b , p ) ¬ T ( k )

[ 15, 16 rezolvense ]

18.

I ( b )

[ S ]

19.

¬ V ( m , k , b ) Z ( b , p ) ¬ T ( k )

[ 17, 18 rezolvense ]

20.

T ( k )

[ S ]

21.

¬ V ( m , k , b ) Z ( b , p )

[ 19, 20 rezolvense ]

22.

¬ Z ( b , p )

[ S ]

23.

¬ V ( m , k , b )

[ 21, 22 rezolvense ]

24.

V ( m , k , b )

[ S ]

25.

[ 23, 24 rezolvense ]

  1. Válaszoljuk meg most a kérdést a szemantikus fa alapklózokkal való lezárásával. A szemantikus fa generálásához elő kell állítani a bázist (az alapatomok egy sorozatát). Alkalmazva a fenti helyettesítést, a bázis kezdő elemei:

A 1

A 2

A 3

A 4

A 5

A 6

R ( m , b )

I ( k )

I ( m )

I ( b )

T ( k )

Z ( b , p )

A 7

A 8

A 9

A 10

A 11

M ( m )

F ( m , k )

V ( m , k , b )

A ( k , b )

O ( m , k )

A szemantikus fa a 11-edik szinten ezzel a báziselemsorrenddel lezárul.

7.1.8. PÉLDA. Tekintsük most a következő programozáselméleti alapkérdést: ha adott egy program és egy inputadat, vajon befejeződik-e a program (megállási probléma) és ha igen, akkor mi lesz a program outputja (válaszprobléma). A kérdés megválaszolásához elő kell állítani a programot leíró formulát és e formulát kell vizsgálni. A formalizálásnál a program egyes alaplépéseit írjuk le (formalizáljuk) és ezt tekintjük a program axiómarendszerének. Ezekből állítjuk elő a programot leíró formulát. Ha ezt a formulát konkrét adatok esetén vizsgáljuk, akkor az említett kérdésekre választ kaphatunk.

A feladat: El kell dönteni, hogy egy adott x egész szám a 7-tel, 9-cel és 11-el való oszthatóságra nézve milyen tulajdonságú. Legyen az output

z { a ha 7 x , b ha 7 | x és 9 x , c ha 7 | x és 9 | x és 11 x , d ha 7 | x és 9 | x és 11 | x .

A tervezett program szerkezeti gráfját az alábbi ábra mutatja.

Az ábrán, illetve leíró nyelvben a predikátumszimbólumok rendre D(x,y), Q1(x,y), Q2(x,y) és QH(x,y), ahol D(x,y) jelentése y|x, Qi(x,y) pedig azt jelenti, hogy a program végrehajtása során az i pont érintésekor mi az összefüggés az x és y között.

A programot leíró formula a következő formulák (a program axiómái) konjunkciója:

  1. x ( ¬ D ( x ,7 ) Q H ( x , a ) )

  1. x ( D ( x ,7 ) Q 1 ( x , x ) )

  1. x y ( Q 1 ( x , y ) ¬ D ( y ,9 ) Q H ( y , b ) )

  1. x y ( Q 1 ( x , y ) D ( y ,9 ) Q 2 ( x , y ) )

  1. x y ( Q 2 ( x , y ) ¬ D ( y ,11 ) Q H ( y , c ) )

  1. x y ( Q 2 ( x , y ) D ( y ,11 ) Q H ( y , d ) )

Vizsgáljuk meg elsőrendű rezolúcióval, előrekövetkeztetéssel a program működését. Állítsuk elő az elsőrendű klózokat.

  1. D ( x ,7 ) Q H ( x , a )

  1. ¬ D ( x ,7 ) Q 1 ( x , x )

  1. ¬ Q 1 ( x , y ) D ( y ,9 ) Q H ( y , b )

  1. ¬ Q 1 ( x , y ) ¬ D ( y ,9 ) Q 2 ( x , y )

  1. ¬ Q 2 ( x , y ) D ( y ,11 ) Q H ( y , c )

  1. ¬ Q 2 ( x , y ) ¬ D ( y ,11 ) Q H ( x , d )

A rezolúciós levezetés az 1–6. klózok és a következő rezolvensek:

  1. ¬ D ( x ,7 ) ¬ D ( x ,9 ) Q 2 ( x , x )

[ 2, 4-ből ]

  1. ¬ D ( x ,7 ) ¬ D ( x ,9 ) ¬ D ( x ,11 ) Q H ( x , d )

[ 6, 7-ből ]

  1. ¬ D ( x ,7 ) D ( x ,9 ) Q H ( x , b )

[ 2, 3-ból ]

  1. ¬ D ( x ,7 ) ¬ D ( x ,9 ) D ( x ,11 ) Q H ( x , c )

[ 5, 7-ből ]

Az 1. és a 8–10. klózok leírják a program input-output kapcsolatát, és egyben mindegyik klóz kijelöl egy utat a gráfban a kiindulópont és a végpont között.

A példabeli program szerkezeti gráfja nem tartalmaz hurkot. Abban az esetben ha a gráf tartalmaz hurkot, akkor azt külön kell leírni, és mint önálló részt felhasználni a leírásban.