III. Szabályalapú logikai következtetés

Speciális szabályalapú következtetés 

III. Szabályalapú logikai következtetés





 Gregorics Tibor

Ismeretalapú modellezés







Mikor alkalmazható a modus ponens (mikor illeszthető egymáshoz két formula) és mi a következménye ? – Ha pq és pqr akkor r (alaki azonosság) – Ha (pq) és pqr akkor r (logikai ekvivalencia) – Ha pq és pr akkor rq (formula részéhez) Elsőrendű formulák esetében az illesztésnél változóhelyettesítésre is szükség lehet. – Ha yP(f(y)) és x(P(x)Q(x)) akkor Q(f(y)). Formai megkötéseket tehetünk a formulák alakjára, hogy az illeszthetőséget könnyen el lehessen dönteni: alaki azonossággal+változó helyettesítéssel Ez azonban a teljesség rovására mehet. Gregorics Tibor







2

Az illesztések egyszerű vizsgálata érdekében a speciális alakú axiómákat és célállítást használunk, miközben törekszünk az állítások eredeti alakjának megőrzésére  ÉS/VAGY formájú (ÉVF) kifejezések – literálok; – AB, AB alakú formulák, ahol az A és B maguk is ÉVF kifejezések. 

Gregorics Tibor


4

Visszafelé haladó szabályalapú reprezentáció

Tény: – univerzálisan kvantált ÉVF kifejezés Szabályok: – LW alakú univerzálisan kvantált kifejezések, ahol L egy literál, a W pedig ÉVF kifejezés Cél: – L1 … Ln alakú egzisztenciálisan kvantált kifejezés, ahol L1, … ,Ln literálok. Gregorics Tibor


1. Reprezentáció

3

Előre haladó szabályalapú reprezentáció 

Gregorics Tibor

1

Illesztés a modus ponens-nél

Ismeretek (tények, szabályok, cél) elsőrendű logikai formulák. Ezek az állítások eredeti formájukat megőrzik, ami másodlagos vezérlési stratégiaként épül be a következtetésbe. Cél: A1, … , An  C tételek bizonyítása, de válaszadásra is alkalmas, amennyiben a kérdést (ki, mit, hol, mikor, mennyiért) egy xP(x) alakú (van-e egyáltalán válasz a kérdésre) célállítással helyettesítjük. Bizonyítás: állítások sorozata, ahol az utolsó állítás a célállítás és amelyben minden állítás – vagy egy tény, – vagy pedig a sorozat megelőző állításaiból és egy szabályból vezethető le a modus ponens alapján. Iránya: előre vagy visszafelé haladó

Tény: – L1 … Ln alakú univerzálisan kvantált kifejezés, ahol L1, … ,Ln literálok.  Szabályok:  WL alakú univerzálisan kvantált kifejezések, ahol L egy literál, a W pedig ÉVF kifejezés  Cél: – egzisztenciálisan kvantált ÉVF kifejezés 

5

Gregorics Tibor


6

1

A formulák átalakítása a Skolem normál formára hozáshoz hasonlóan megy 





Akadályok Előre haladó

Szabályokban visszaállítjuk a főimplikációt – (minden más implikációt eliminálunk) Célállítást fordítva Skolemizáljuk – Az univerzális kvantoroktól szabadulunk meg Nem alkalmazzuk a disztributív törvényeket – Emiatt nem tudjuk a lehető legáltalánosabb változó-átnevezést alkalmazni, csak főkonjunkciós tényezőnként.

 



– –

Gregorics Tibor




Több tényből könnyű egyet csinálni  Nem megfelelő alakú tény esetén (L1…Li)…(Lo …Lz)  Nem megfelelő alakú szabály 

L1  L2  W helyett L1 W és L2 W L1  L2 W ?

– –

Gregorics Tibor

7

2. Gráfreprezentáció 

Visszafelé haladó

Több tényből könnyű egyet csinálni Nem megfelelő alakú cél esetén (L1…Li)…(Lo…Lz) Nem megfelelő alakú szabály

W  L1  L2 helyett WL1 és WL2 W  L1  L2 ? Ismeretalapú modellezés

8

Illesztés ÉS/VAGY gráfba rajzolása Tény: P(a)Q(b) Szabály: P(x)R(x)S(x) Cél: R(z)Q(y)

A megcélzott logikai következtetést egy alkalmas gráfbeli út megkeresésének problémájává fogalmazzuk át. A logikai reprezentációnak egy ÉS/VAGY gráfot feleltetünk meg, amelynek hiperútja egy-egy bizonyítást szimbolizál.

P(a)Q(b)

P(a) xa P(x)

A „vagy” művelet ÉS kapcsolatot indukál

Q(b) yb Q(y)

L, L’W, L =L’  W

R(a) R(x) L, L =L’  L’

S(a) S(x)

Az „és” művelet VAGY kapcsolatot indukál

z a R(z)

Gregorics Tibor


Gregorics Tibor

9

P(x)Q(y) Az „és” művelet ÉS kapcsolatot indukál

P(x) xx1 P(x1)

Q(y) yb Q(b)

W, WL’, L =L’  L

R(x1) L’, L =L’  L Gregorics Tibor

x1a

S(x1)

A „vagy” művelet VAGY kapcsolatot indukál

10

Előre haladó szabályalapú gráfreprezentáció

Illesztés ÉS/VAGY gráfba rajzolása Tény: Q(b)R(a) Szabály: R(x)S(x)P(x) Cél: P(x)Q(y)




olyan (R,s,T), ahol  R=(N,A) egy ÉS/VAGY gráf, amelyet a tény ÉS/VAGY gráfjából kiindulva építhetünk fel úgy, hogy az összes lehetséges módon illesztjük a szabályokat és a célliterálokat,  s - tényállítást szimbolizáló csúcs,  T - célliterálokat szimbolizáló csúcsok.

R(a) Ismeretalapú modellezés

11

Gregorics Tibor


12

2

Visszafelé haladó szabályalapú gráfreprezentáció 

Megjegyzés A reprezentációs gráf mindig egy fa. Egy szabály illetve (cél/tény) literál többször is illeszthető.  A logikai levezetés (bizonyítás) egy megoldásgráfként (sT hiperút) jelenik meg a gráfban.  Nem minden megoldásgráf jelent levezetést.

olyan (R,s,T), ahol  R=(N,A) egy ÉS/VAGY gráf, amelyet a cél ÉS/VAGY gráfjából kiindulva építhetünk fel úgy, hogy az összes lehetséges módon illesztjük a szabályokat és a tényliterálokat,  s - célállítást szimbolizáló csúcs,  T - tényliterálokat szimbolizáló csúcsok.

Gregorics Tibor


 

Gregorics Tibor

13

Ellentmondásos levezetés Tény: A(x)B(x)



A(x)B(x)

A(x) xa A(a)

Gregorics Tibor

B(x) 



xb B(b)




Ha 1, … , m helyettesítések konzisztensek, akkor nem írnak elő ugyanarra a változóra olyan {xti} helyettesítéseket, amelyek termjei nem egyesíthetőek:  

  

Gregorics Tibor




o o



17

16

A reprezentációs gráfban történő irányított út (megoldási gráf) keresése visszalépéses kereséssel o

Az egyesítő helyettesítés független az 1, … , m helyettesítések sorrendjétől. A helyes levezetés egy ellentmondásmentes illesztőhelyettesítéseket tartalmazó megoldásgráf. Az EK-t válaszadásra is felhasználhatjuk.


3. Következtetés

={xa} és ={ya} konzisztens ={xy} és ={xa, yb} inkonzisztens

Gregorics Tibor

Az 1, … , m helyettesítések (i={vi1ti1, … ,vinitini}) konzisztensek (ellentmondásmentesek), ha a V=< v11 , … , vmnm > és T=< t11 , … , tmnm > sorozatok egyesíthetők. A V és T legáltalánosabb egyesítőhelyettesítését az 1, … , m helyettesítések egyesítő kompozíciójának (EK) nevezzük.

15

Megjegyzés

14

Konzisztencia és az egyesítő kompozíció 

Cél: A(a)B(b)


Globális munkaterületen a startcsúcsából induló hiperút Szabályok: az illesztések illetve a visszalépés Visszalépéses vezérlési stratégia • Másodlagos stratégiák: formulák alakjának felhasználása • Heurisztikák

A talált megoldási gráf konzisztenciájának ellenőrzése Gregorics Tibor


18

3

Példa

Tény vagy szabály? 

Tomi és Misi tagjai az alpinisták klubjának. Egy klubtag síelő vagy hegymászó. Nincs olyan hegymászó, aki szeretné az esőt. A havat minden síelő szereti. Tomi szereti az esőt és a havat. Misi mindenben ellentétesen vélekedik, mint Tomi.

• 

Nem egyértelmű esetek

•

x(H(x)Sz(x,eső)) helyett x(H(x)  Sz(x,eső) ) y (Sz(Tomi,y)  Sz(Misi,y) ) y (Sz(Tomi,y)  Sz(Misi,y) )

• •

Ki az a klubtag, aki hegymászó, de nem síelő?

Gregorics Tibor


Egyértelmű esetek

A(Tomi)  A(Misi)  Sz(Tomi,eső)  Sz(Tomi,hó) x (A(x)  S(x)  H(x) ) x (S(x)  Sz(x,hó) )

•

•

Gregorics Tibor

19


Szabályok formája 



Gregorics Tibor


Válasz 

szabály szétbontása – x (A(x)  S(x)  H(x ) ) helyett x (A(x)  S(x)  H(x) ) x (A(x)  H(x)  S(x) ) szabály átformálása (kontrapozitív alak) – y (Sz(Tomi,y)  Sz(Misi,y) ) mellett y (Sz(Misi,y)  Sz(Tomi,y) )



21

Kérdés: Ki az az x személy, aki A(x)  H(x)  S(x) Cél: x ( A(x)  H(x)  S(x) )

Gregorics Tibor

Következtetési irány megválasztása 

Tény:



Szabály:

–

– – – – – –



20


22

Tény illesztése a szabály illesztése előtt

A(Tomi)  A(Misi)  Sz(Tomi,eső)  Sz(Tomi,hó) A(x)  H(x)  S(x)

A(x)  S(x)  H(x) A(x)  H(x)  S(x) S(x)  Sz(x,hó) H(x)  Sz(x,eső) Sz(Tomi,y)  Sz(Misi,y) Sz(Tomi,y)  Sz(Misi,y)

A(x)

S(x)

{xTomi} A(Tomi) tény

Cél: A(x)  H(x)  S(x) Gregorics Tibor

H(x)


23

Gregorics Tibor

A(Misi) 1. szabály

kontrapozitív 3. szabály


24

4

Példa folytatása {x2x}

A(x)  H(x)  S(x) A(x)

H(x) {x1x}

{xTomi} A(Tomi)

S(x)

H(x1)

{xMisi, yhó} Sz(Misi,y)

A(x)


V=<x, x1, x | x2 , y, x, x2, y, x | x2, y1, x, x21, y1, x > T= 25

Gregorics Tibor

S(x) H(x) {x1x}  ={ x/T, x1 /x } H(x1)

A(x)

{xTomi}

 ={ x/T, x1 /x }

S(x)


A(x)  H(x)  S(x)

Sz(x,hó) {xMisi, yhó} Sz(Misi,y)  = ?

A(x) {xTomi} A(Tomi)

H(x1) S(Tomi)


27

Gregorics Tibor


Additív módon számolt aktuális egyesítő kompozíció – Az aktuális hiperút konzisztenciáját vizsgáljuk. •



A(x)  H(x)  S(x)

Ha ellentmondásos, akkor visszalépünk. Ha nem (van EK), tovább lépünk; ezután elég a soron következő illesztő helyettesítés és a korábban talált EK konzisztenciáját megvizsgálni. (additív számolás)

A(x) {xTomi} A(Tomi)

 Aktuális EK tárolása minden csúcsnál. Változó behelyettesítés a hiperút párhuzamos ágain – Egy változóra vonatkozó helyettesítést, nemcsak az illesztés alatt, hanem az aktuális hiperútban mindenhol érvényesítjük. – Változó helyettesítés előtti állapot hisztorizálása. Gregorics Tibor


28

Példa folytatása: visszalépések

Folyamatos konzisztencia ellenőrzés

•

Sz(Tomi,hó) ?

A(Tomi)

Gregorics Tibor



{x2Tomi} S(x2)

H(x) H(Tomi) S(x) S(Tomi) {x1Tomi}

A(Tomi)

Sz(Tomi,hó)

A(Tomi)

26

Ellentmondás korai felismerése 2.

{x2x} ={ x/T, x1 /x, x2x } A(x)  H(x) S(x) S(x2)

A(x) {xTomi}  = {x/T} A(Tomi)

x21,y1

A(Tomi)

Ellentmondás korai felismerése 1. =Ø

S(x)

x2,y

Sz(Tomi,hó)

Gregorics Tibor

A(Tomi)

Sz(Tomi,hó)

A(Tomi)

S(x)

H(x)

A(x) Sz(x,hó)

S(x)

A(x)

A(x)  H(x)   S(x)

S(x2)

H(x1)

{xTomi}

Ismétlődő szabálykapcsolat-gráf

 S(x) S(Tomi) H(x) H(Tomi) {x1Tomi}

A(Tomi)

H(x1)

{x2Tomi} S(x2) Sz(Tomi,hó) ?

S(Tomi)

A(Tomi) 29

Gregorics Tibor


30

5

Példa folytatása a sorozatos visszalépések után {x2Misi} S(x2)

A(x)  H(x)  S(x) A(x)

{xMisi}

A(Misi)

Másodlagos stratégiai elemek

H(x1)

Sz(Misi,y)

o o

Következtetési irány megválasztása Szabályalkalmazások iránya Tény illesztése a szabály illesztése előtt

Folyamatos konzisztencia ellenőrzés Illesztő helyettesítés iránya: fentről lefelé  Ismétlődő szabálykapcsolat-gráf 

S(Misi)



Sz(Tomi,hó) A(Misi)

Szabályok jellemző alakja o

Sz(Misi,hó) {yhó}

{x1Misi}

A(Misi)



S(x) S(Misi)

H(x) H(Misi)

V=< x, x1, x, x2, y, x> T=<M, x, M, x, hó, M>

Gregorics Tibor

Sz(Tomi,hó)


31

Gregorics Tibor


Sorrendi heurisztikák 



Kiértékelő függvény – az adott pillanatban illeszthető literálok (tények illetve szabályok) rangsorolására Meta-szabály – az adott pillanatban illeszthető literálok (tények illetve szabályok) rangsorolására

1. Példa Azt a literált válasszuk, amelyikhez a legkevesebb féle illesztést alkalmazhatjuk! Tény: képviselők, ácsok, szülő-gyerek párok Cél: Szülő(y,x)  Ács(y)  Képviselő(x) Szülő(y,x)

Gregorics Tibor


33

1. Példa Szülő(u,v)

Szülő(a,v)

Szülő(u,a)

Szülő(a,b)

1 000 000

12

2

1

Ács(u)

Ács(a)

10 000

1

Képviselő(u) Képviselő(a) 350 Gregorics Tibor

Képviselő(x) Ismeretalapú modellezés

Lehetséges próbálkozások száma a Szülő, Ács, Képviselő rögzített illesztési sorrendje mellett: Szülő, Ács, Képviselő: 1 000 000*1*1 Ács, Képviselő, Szülő: 10 000*350*1 Ács, Szülő, Képviselő: 10 000*12*1 Képviselő, Ács, Szülő: 350*10 000*1 Képviselő, Szülő, Ács: 350*2*1

Ács(y) Ács(b)

Képviselő(x)

1 0002000

101000

350

Gregorics Tibor

?

Ács(b)

34

1. Példa

Szülő(y,x) Szülő(y,a)

Szülő(b,a) 35

Ács(y)

Gregorics Tibor

y/b

1 Ismeretalapú modellezés

32

x/a

Képviselő(a) Ismeretalapú modellezés

36

6

2. Példa Mindig a fontosabb szabályt illesszük!

4. A SZK nem teljes módszer 

A reprezentáció korlátjai miatt – Nem minden logikai reprezentáció írható át csak előre vagy csak visszafelé haladó szabály alakúra



A következtetés korlátjai miatt – Nem minden tétel vezethető le szabályalapú következtetéssel. LL

Ha az alábbi szabályok közül mindkettő illeszthető

(Milyen irányú az L1  L2  L3  L4 szabály?)

1. „ha a betegnek leállt a szíve, akkor szívmasszázst kell alkalmazni” 2. „ha a betegnek horzsolt seb van az alkarján, akkor be kell kötözni”

Tény: Szabályok: Cél: LL

akkor az elsőt kell alkalmazni. Gregorics Tibor


37

Gregorics Tibor

L

? Ismeretalapú modellezés

L 38

7

III. Szabályalapú logikai következtetés

Recommend Documents