|
Time je formirana jedna OL-rezolventa datih sastavaka. Za centralni i bočni sastavak mogu nastati sledeći slučajevi: - ne postoji OL-rezolventa, - rezolventa je tautologija, pa se zato isključuje, - rezolventa je prazan sastavak p, - postoji više različitih Ol-rezolventi (za poslednji literal centralnog sastavka i različite k-te literale u bočnom sastavku). 18. Sistem ADT sa rezol, indukc, simetrij. Dokaz u obliku pobijanja zasniva se na sledećim pravilima izvođenja: uređena linearna rezolucija sa markiranim literalima (OL-rezolucija), pravilo binarne indukcije (pravilo P) i pravilo simetrije. Kao ulazni podatak u sistem može se pojaviti rečenica ograničenog engleskog jezika ili predikatska formula. Polazni skup od kojeg startuje sistem ADT sadrži sastavke koji potiču od premisa na koje se dokaz tvrđenja može osloniti. Sastavci koji potiču od shema-aksioma matematičke indukcije ili simetrije se ne uključuju u polazni skup, jer ih u sistemu zamenjuju pravilo indukcije i pravilo simetrije. Uređena linearna rezolucija sa markiranim literalima, , izabrana je zbog prednosti koja se ogleda u potrebi memorisanja samo onih sastavaka koji su generisani na uzastopnim (susednim) nivoima, a ne svih generisanih sastavaka u procesu traženja dokaza. . Osim toga, jedan od sastavaka koji učestvuju u OL-rezoluciji je na svakom koraku unapred fiksiran u svojstvu "centralnog sastavka", a rezolucija (ili indukcija) vrši se samo po njegovom poslednjem literalu. Drugi sastavak uzima se iz skupa polaznih sastavaka i ima ulogu "bočnog sastavka". S obzirom da primena pravila indukcije dovodi do generisanja dva sastavka, jedan od njih se zadržava u svojstvu kandidata za novi centralni sastavak na narednom nivou, a drugi se zapisuje u polazni skup bočnih sastavaka. U sistemu se koristi i sledeće pravilo simetrije. Ako bi polazni skup sadržao sastavak koji izražava aksiomu simetrije ØR(x,y) Ú R(y,x), onda bi došlo do generisanja nepotrebnih sastavaka. Da bi se to izbeglo u sistem je implementirano pravilo simetrije. ( Da li treba pravilo simetrije ? ) 19. Proširenje met. rezolucije- paramodulac; i indukc Pravilo paramodulacije Iz sastavka D1:P(t) Ú C1 i D2: r = s Ú C2 , koji ne sadrže zajedničke promenljive (gde su C1 i C2 sastavci, r i s termi, a P(t) literal koji sadrži term t) pod uslovom da postoji NOU s za t i r, izvodi se tzv. binarni paramodulant sastavaka D1 i D2: Ps(ss) Ú C1s Ú C2s gde Ps(ss) označava rezultat zamene jednog ulaženja terma ts u Ps termom ss. Paramodulacija je izvođenje paramodulanata iz roditeljskih sastavaka. E-pobijanje je konačan niz sastavaka B1,...,Bm u kojem za svaki član Bi važi: - Bi Î S , S je polazni skup sastavaka, ili - Bi je rezolventa ili paramodulant nekih prethodnih članova, i - Bm je prazan sastavak. Slično kao za rezoluciju, i za paramodulaciju se mogu razmatrati različite restrikcije s ciljem povećanja efikasnosti procedure traženja pobijanja. Prilikom razrade restrikcija za primenu pravila paramodulacije pažnja se usmerava na kriterijume za izbor terma koji će učestvovati u generisanju paramodulanta. Ovi kriterijumi se odnose ili na izbor relevantnog terma ili na nalaženje užeg skupa terma koji su perspektivni, uz odbacivanje neperspektivnih terma. Neka polazni skup formula sadrži sledeću shemu-aksioma matematičke indukcije: Ax(0) Þ ("y (Ax(y) Þ Ax(Sy)) Þ "x A(x)) gde je A(x) - proizvoljna predikatska formula, Sx - naslednik od x, Ax(t) - oznaka za formulu određenu iz A(x) zamenom svakog slobodnog ulaženja promenljive x termom t, pri čemu je term t slobodan za x u formuli A(x), i promenljiva y ne ulazi u A(x). Iz ove sheme-aksioma mogu se dobiti dva kvazi-sastavka na koje je primenljiva f-tehnika Darlingtona, ali sa istim nedostacima kao u slučaju jednakosne supstitucije. Ovi nedostaci se eliminišu uvođenjem posebnog pravila indukcije. Pravilo binarne indukcije (Hotomski P., 1982.) omogućuje da se sastavci koji potiču od sheme-aksioma matematičke indukcije eliminišu iz polaznog skupa sastavaka. To oslobađa od rada sa proizvoljnom formulom (formulskom promenljivom) koja figuriše u aksiomi indukcije, doprinosi smanjivanju broja generisanih sastavaka i skraćivanju dokaza. 21. Izrada kombinovanih rasporeda-konc.sis.DEDUC 23. Veza sastavaka sa klauzulama prologa Prva stepenica u nastojanju da se rezolucijskom dokazu pridruži prirodnija forma je transformisanje zapisa sastavaka u implikativan oblik. To se može postići na sledeći nain. Neka je D sastavak oblika L1 Ú L2 Ú ... Ú Lk , gde su Li literali (atomične firmule ili njihove negacije). Na osnovu tautologija ØpÚqÛ(pÛq); Ø(pÚq)ÛØpÙØq; ØØpÛp, za svako j, 1 £ j £ k, važi: ÙØLi Þ Lj iÎ{1, . . . ,k}\{j} Na taj način, sastavku D može se pridružiti k različitih implikativnih zapisa. Oblik u kojem sa desne strane implikacije stoji pozitivan literal (bez negacije) je intuitivno najprihvatljiviji. On je moguć pod uslovom da izvorni sastavak sadrži bar jedan pozitivan literal. Sastavci koji sadrže bar jedan pozitivan literal zovu se Hornovi sastavci. Primena pravila rezolucije u ovakvoj notaciji svodi se na unifikaciju cilja sa desnom stranom neke implikacije ili sa nekim literalom kada u izrazu nema implikacije. Time je praćenje dokaza bitno olakšano s obzirom da se radi bez eksplicitne negacije polaznog tvrđenja. Još prirodnijem tumačenju pobijanja doprinosi shvatanje formule koja sadrži implikaciju kao pravila, a formule bez implikacije kao činjenice. Pravilo N(b,x)ÞN(a,x) zapisuje se u sledećem obliku: N(a,x):-N(b,x). Takav zapis zove se klauzula. Uopšte, pravila su klauzule: zaključak:-pretpostavka, ..., pretpostavka gde je zaključak pozitivan literal, a pretpostavke su literali sa ili bez negacije. Zaključak je glava klauzule, a pretpostavke sačinjavaju telo klauzule. Svaki Hornov sastavak može se zapisati u formi pravila, odnosno u obliku klauzule. Zaista, ako je L pozitivan literal, onda se L1Ù... Ù LkÞL zapisuje kao klauzula: L:-L1,...,Lk. Literali u telu klauzule mogu sadržati simbol negacije. Činjenica N(b,c) može se tretirati kao klauzula sa praznim telom - klauzula koja se sastoji samo od glave. Time se primena pravila rezolucije svodi na unifikaciju cilja sa glavom klauzule, pri čemu se dobija q-primer tela klauzule u svojstvu novog podcilja Ciljevi koji sadrže samo jedan literal zovu se upiti. Uopšte, cilj može sadržati više literala, U tom slučaju pojedini literali kao elementi cilja, razdvajaju se zarezom. Ustvari takav cilj dobija se rezolucijom sa klauzulom koja u telu sadrži više literala, kao na primer Prethodno sprovedena razmatranja mogu se ovako rezimirati: 1. Restrikcijom na Hornove sastavke i razlikovanjem ciljeva od klauzula (pravila i činjenica), rezolucijsko pobijanje se može transformisati u pregledan, semantički prihvatljiv i razumljiv oblik. 2. Zadovoljenje elementa cilja svodi se na unifikaciju tog elementa sa glavom neke klauzule. Pri tome se generiše novi podcilj u koji se uključuju q-primeri svih literala iz tela te klauzule i zadržavaju se q-primeri preostalih elemenata cilja. 3. Zadovoljenje početnog cilja postiže se uzastopnim generisanjem podciljeva sve dok i poslednji element podcilja bude zadovoljen generisanjem praznog podcilja. 4. Zbog restrikcije na Hornove sastavke, koja je u vezi sa zahtevom da glava klauzule bude pozitivan literal, neki od klasičnih rezolucijskih dokaza ne mogu biti prevedeni u navedeni oblik klauzula. Takvi su na primer, svi oni dokazi pobijanjem koji bitno zavise od sastavaka koji sadrže bar dva negativna literala i ne sadrže ni jedan pozitivan literal. 5. Navedena restrikcija ipak dopušta automatsko zadovoljenje velikog broja raznovrsnih ciljeva na osnovu pretpostavki, zapisanih u obliku pravila i činjenica. Veliki broj praktično značajnih zadataka i uslova za njihovo rešavanje, mogu se izraziti u obliku ciljeva i klauzula. Skup klauzula predstavlja bazu znanja za zadovoljenje cilja.
 |
RSS link na komentare