P rz yk ła d : św ia t w u m p u sa

R e p re ze n ta cj a w ie d zy w ję zy k u lo g ik i

Metodyprzeszukiwaniawprzestrzenistanówsformułowanebyływpostacidość ogólnej,jednakwymagałyreprezentacjizagadnieniawewłaściwejformie,tzn. przestrzenistanów,zbioruoperatorów,adodatkowoprzydatna/potrzebnabyła informacjaheurystycznawformiefunkcjiocenystanów. Ogólnie,formatisposóbreprezentacjiwiedzyozagadnieniusąniezwykleistotneimają bezpośredniwpływnaefektywność—lubwogólezdolność—znalezieniarozwiązania. Istniejeszeregopracowanychogólnychpodejśćdoproblemureprezentacji,iróżne reprezentacjemajązwyklezwiązaneznimitechnikiwnioskowania,czyliformowania pewnychustaleńpomocniczych(wniosków),mogącychsłużyćdoznalezienia ostatecznegorozwiązaniaproblemu. Jednymznajpopularniejszychschematówreprezentacjiwiedzyjestjęzyklogiki matematycznej. Metodyopartenalogice—reprezentacjawiedzywjęzykulogiki1 Dlaczegologikamatematycznajestdobrymjęzykiemreprezentacjiwiedzydlasztucznej inteligencji? Zjednejstrony,języklogikijestzbliżonydosposobuwjakiludziemyśląoświecie, imyśliswewyrażająwzdaniachjęzykanaturalnego.Czasamimówisiękolokwialnie,że człowiekmyśli„logicznie”.Kategorie,którymimyśliimówiczłowiekobejmujątakie konstrukcjejak:obiekty,związkimiędzyobiektami(relacje),stwierdzeniafaktów prostychizłożonych,zdania,spójnikizdaniowe,wyrażeniafaktówwarunkowych, anawetkwantyfikatory. Zdrugiejstrony,logikamatematycznadostarczaprecyzyjnegoaparatuwnioskowania opartegonadowodzeniutwierdzeń.Ludzie,myśląc,równieżstosująpodobne wnioskowanielogiczne,zatemaparatlogikimatematycznejwydajesiędobrąplatformą reprezentacjiwiedzyagentainteligentnego,któregosposóbwyrażaniafaktów iwnioskowaniabyłbyzbliżonydoludzkiego. Metodyopartenalogice—reprezentacjawiedzywjęzykulogiki2

P rz yk ła d : św ia t w u m p u sa

Dosprawdzeniadziałaniawielumetodprzydatnejestśrodowiskotestowedostatecznie proste,abymożnabyłointuicyjnieokreślaćwłaściwereprezentacjeisprawdzaćproste koncepcje,alejednocześniedostateczniebogate,abypozwoliłokonfrontowaćte metodyzcorazbardziejrealnymiprzeszkodami. Jednymztakichtestowychśrodowiskpodręcznikowychjestświatwumpusa.1Wtym środowiskuporuszasięagentdążącydoznalezieniazłota(ibezpiecznegowyniesienia gozjaskini).Naprzeszkodziestojązapadliny(pits),wktóreagentmożewpaść, ipotwór(tytułowywumpus),którymożeagentazjeść. Agentmożejedynieobracaćsięwprawolubwlewo,poruszaćsiępojednymkrokudo przodu,wystrzelićzłukujedynąposiadanąstrzałę(nawprost),podnieśćzłoto,gdyje znajdzie,iwyjśćzjaskini,jeśliznajdujesięwpunkciestartowym. 1PrzedstawionetuprzykładyidiagramyświatawumpusazaczerpniętezostałyzpodręcznikaRussellaiNorviga„Arti- ficialIntelligenceAModernApproach”imateriałówudostępnionychnastronieinternetowejStuartaRussella. Metodyopartenalogice—światwumpusa3 Agentotrzymujepewneinformacjeośrodowisku(daneotrzymywanezreceptorów agentanazywasięperceptami):wyczuwasmródwumpusa(stench)ipowiew powietrzazzapadlin(breeze),jeśliznajdujesięwpolusąsiadującymznimi.Ponadto zauważazłoto(gold),aletylkojeślijestwtymsamympolucoono.Niemożejednak sprawdzićswojejbezwzględnejpozycji(àlaGPS),możejedyniesamswojąpozycję rejestrować.Ścianyjaskiniwyczuwajedynieprzezpróbywejściawnie,którepowodują odbicia. BreezeBreeze

Breeze

BreezeBreeze Stench

Stench

Breeze PIT PIT PIT 1234

1

2

3

4 START

Gold

Stench Metodyopartenalogice—światwumpusa4

P rz yk ła d : p o ru sz a n ie si ę w św ie ci e w u m p u sa

A

OK OKOK

OK OKOK

A A

BOK OKOK

A A

B

P? P? OK OKOK

A A

B

P? P? A

S

OK OKOK

A A

B

P? P? A

S

OK

P W

OK OKOK

A A

B

P? P? A

S

OK

P W

A Metodyopartenalogice—światwumpusa5

P rz yk ła d : p o ru sz a n ie si ę w św ie ci e w u m p u sa (c d .)

OK OKOK

A A

B

P? P? A

S

OK

P W

A

OK OKOK

A A

B

P? P? A

S

OK

P W

A

OK

OK OK OKOK

A A

B

P? P? A

S

OK

P W

A

OK

OK A

BGS Jednakniezawszemożna skuteczniedziałaćwświecie wumpusaposługującsiętylko wnioskowaniemlogicznym. Wniektórychprzypadkach jedynymrozwiązaniemjest „strzelanie”,czyliwybórruchu naślepo,idopieropotem analizowaniesytuacji. Oczywiścieoileprzeżyjemy!!

A

BOK OKOK A

B A

P? P? P? P?A

S Metodyopartenalogice—światwumpusa6

R a ch u n e k p re d yk a tó w p ie rw sz e g o rz ę d u — te rm y

Termyreprezentująwjęzykulogikiobiekty,imogąbyć:stałymi(oznaczająkonkretny obiekt),zmiennymi(mogąprzybieraćwartościróżnychobiektów),lubfunkcjami (wyznaczająjakiśobiektnapodstawiewartościswoichargumentów,inaczej,przypisują jednymobiektominne). Przykładytermów:A,123,x,f(A),f(g(x)),+(x,1) Umowniezapisujemytermystałewielkimiliterami,azmiennemałymi. Zauważmy,żewpowyższychprzykładachostatnitermjestniejawnymzapisem następnikax,anieoperacjąodejmowania.Wczystejlogiceniemaodejmowania. Będziemymielidoczynieniaztymproblememwwielusytuacjach. Metodyopartenalogice—rachunekpredykatów7

R a ch u n e k p re d yk a tó w p ie rw sz e g o rz ę d u — p re d yk a ty

Predykatyreprezentująrelacjenazbiorzetermów.Możemyjetraktowaćjakofunkcje mającewartośćprawdylubfałszu(1lub0),któreprzypisująprawdękażdejn-ce termówspełniającychrelację,afałszkażdejn-ceniespełniającej. Zapispredykatuzzestawemtermównazywamyformułąatomową. Przykładyformułatomowych:P,Q(A),R(x,f(A)),>(x,10) Zapisfunkcyjny:>(x,10)jestodpowiednikiemrelacji:x>10.Warytmetyce potraktowalibyśmytakizapisjakonierównośćimoglibyśmyjąrozwiązywać.Natomiast formułylogicznemożemyjedyniewartościować,toznaczywyznaczaćichwartość logicznąprawdylubfałszu.Gdyformułazawierazmiennątoczęstoniedasię wyznaczyćjejwartościlogicznej. Metodyopartenalogice—rachunekpredykatów8

R e p re ze n ta cj a fa k tó w za p o m o cą fo rm u ł

Jakisensmajęzyklogikipredykatów? Możemyprzyjegoużyciuopisaćfakty,którechcemywyrazić,np.: At(Wumpus,2,2) At(Agent,1,1) At(Gold,3,2) Wybórzestawusymboli,którymizamierzamyopisaćobiektyirelacjepewnegoświata, nazywamykonceptualizacją.Naprzykład,alternatywnadopowyższej konceptualizacjaświatawumpusamogłabyzawieraćformuły: AtWumpus(loc(2,2)) AtAgent(loc(1,1)) AtGold(loc(3,2)) Powyższekonceptualizacjesąpodobne,aczkolwiekmająniecoodmiennewłaściwości, np.wdrugiejwumpus,agent,anizłotoniewystąpiąwjawnejpostaci.Ogólnieod przyjętejkonceptualizacjimożezależećłatwość,anawetmożliwośćwyrażaniaróżnych faktówodziedzinieproblemowej. Metodyopartenalogice—rachunekpredykatów9

R e p re ze n ta cj a fa k tó w za p o m o cą fo rm u ł (c d .)

Przykłademproblemukonceptualizacyjnegoświatawumpusajestopisistnienia ipołożeniadziur.Możemynadaćdziuromprawaobywatelskieitożsamość: At(Pit4,3,3) Wtensposóbmożemyłatwoopisaćcałyświatwidzianyzlotuptaka,nadając poszczególnymdziuromdowolniewybranenazwy(termystałe).Zpunktuwidzenia agentaporuszającegosięwświeciewumpusatakonceptualizacjajestjednakbardzo niewygodna.Trudnobyłobywtensposóbopisaćświatstopniowopoznawany,gdyna początkuagentnieznanawetliczbydziur.Istnieniedziurytrzebawtedyopisać zmienną: At(x,3,3) Jednakztegozapisuniewynika,żexjestdziurąiwymagatouzupełniającychopisów. Wygodnąalternatywąjestpostrzeganiedziurjakoanonimowych,itylkozapisywanie faktówistnienialubnieistnieniadziurwkonkretnychmiejscach: PitAt(3,3) NoPitAt(1,1) Metodyopartenalogice—rachunekpredykatów10

S p ó jn ik i lo g ic zn e i fo rm u ły zł o żo n e

Formułyzłożonejęzykapredykatówpierwszegorzędumożnakonstruowaćza pomocąspójnikówlogicznychtakichjak:¬,∧,∨,⇒,⇔.Jakoszczególny przypadek,formułęktórajestformułąatomowąlubnegacjąformułyatomowej nazywamyliterałem. Przykładyformułzłożonych(pierwszajestpojedynczymliterałem): ¬At(Wumpus,1,1) PitAt(2,1)∨PitAt(1,2) [At(Agent,1,1)∧PitAt(2,1)]⇒Percept(Breeze) Zauważmy,żeostatniaformułajestzupełnieinnejnatury,niżdwiepierwsze.Dwie pierwszeformułymogąstanowićfragmentopisuświataotrzymanegoi/lub budowanegoprzezagentainteligentnegowtrakciejegopracywświeciewumpusa. Natomiastostatniaformuławyrażajednozprawświatawumpusa.Agentznato prawo,imożeposiadaćtakąformułęwswojejbaziewiedzy. Faktyogólniesłusznewdanejdziedzinieproblemowejnazywamyaksjomatami świata.Natomiastfaktyopisującestankonkretnejinstancjiproblemu,nazywamy incydentalnymi. Metodyopartenalogice—rachunekpredykatów11 Wartojeszczepodkreślić,że⇒i⇔sątylkospójnikamilogicznymi,tworzącymizpary dowolnychformułformułęzłożoną.Niemająonenicwspólnegozprocesem wnioskowania,którybędzierozważanyponiżej. Metodyopartenalogice—rachunekpredykatów12

K w a n ty fi k a to ry

Formułyzłożonemożnarównieżbudowaćzapomocąkwantyfikatorów:∀,∃,które wiążązmiennewformułach.Ogólnyschematformułyzkwantyfikatorem: ∀xP(x) Zmiennąniezwiązanąkwantyfikatoremwformulenazywamywolną.Formuła: ∃yQ(x,y) zawieradwiezmienne,jednąwolną,adrugązwiązanąkwantyfikatorem. Zdaniemnazywamyformułębezwolnychzmiennych. Przykłady: ∃x,yAt(Gold,x,y) ∀x,y[At(Wumpus,x,y)∧At(Agent,x,y)]⇒AgentDead ∀x,y[At(Wumpus,x,y)∧At(Agent,−(x,1),y)]⇒Percept(Stench) Zwróćmyuwagę,żewostatnimprzykładzie−(x,1)jestniejawnymzapisem współrzędnejnalewoodx,anieodejmowaniem.Wlogiceniemaodejmowania. Metodyopartenalogice—rachunekpredykatów13

K ró tk ie p o d su m o w a n ie — p yt a n ia sp ra w d za ją ce

1.Opracujkompletnąkonceptualizacjęświatawumpusawrachunkupredykatów pierwszegorzędu.Toznaczy:wprowadźsymboletermów(stałychifunkcji termowych),orazsymbolepredykatówniezbędnedoopisywaniainstancjiproblemów wtejdziedzinie. Uwaga:nierozważamyprocesuposzukiwaniarozwiązania,analizyalternatywnych ruchówiichskutków,opisywaniasekwencjikroków,itp.Poszukujemyjedynie formatupozwalającegonastatycznyopisstanuzagadnienia,tzw.snapshot. 2.Wykorzystującreprezentacjęopracowanąwpoprzednimpunkcie,opiszinstancję problemuprzedstawionąnastronie4. 3.Spróbujzapisaćaksjomatykęświatawumpusa,toznaczy:ogólneregułyrządzące tymświatem. Metodyopartenalogice—rachunekpredykatów14

S e m a n ty k a — in te rp re ta cj e

Definicjajęzykapredykatówokreśliłajednąskładowąreprezentacji,tzn.jegoskładnię, inaczejsyntaktykę.Drugąskładowąjestsemantyka,czyliaparatpozwalający określaćznaczenia. Napozór,znaczenieniektórychformułmogłobywydawaćsięjasne.Dotychczas intuicyjniedomyślaliśmysięcoznaczyAt(Agent,2,2).Wogólnościtojednaknie wystarczy.Nawetograniczającsiędoświatawumpusa,niewiadomoktórejturygry iktóregostanutejgrydotyczypodanaformuła. Interpretacja–przypisaniesyntaktycznymelementomjęzykapredykatów(termom ipredykatom)obiektówzjakiejśkonkretnejdziedziny(świata). Woczywistysposób,konkretnaformułazapisanaprzyużyciupewnegozestawu symbolimożedotyczyćróżnychdziedzin.Naprzykład,formułaAt(Agent,2,2)może odnosićsiędopewnejturywumpusa,scenyzfilmuoagencie007,jakiegośagentaze światarzeczywistego,albojeszczeinnegoagenta. Możliwychinterpretacjidladanejformułymożebyćbardzowiele. Metodyopartenalogice—semantykarachunkupredykatów15

M o d e le

Zauważmy,żeinterpretacjaokreślaprawdziwośćformułatomowych.Jeśliwdanej dziedziniezachodzirelacjamiędzypewnymiobiektami,toformułazapisującatoza pomocąodpowiednichtermówipredykatujestprawdziwawtejinterpretacji. Równieżnaodwrót,majączapisanądowolnąformułę,możemywyznaczyćjejwartość logicznąsprawdzającczywdanejinterpretacjizachodziopisanyprzezformułęzwiązek. (Jednakgdyformułazawierazmiennewolnetojejprawdziwośćmożeniebyćokreślona przezinterpretację.) Konsekwentnie,korzystajączdefinicjispójnikówlogicznychikwantyfikatorówmożemy wyznaczyćwartośćlogicznądowolnejformuły(zdania)dladanejinterpretacji.Możemy więcmówić,żeinterpretacjeokreślająprawdziwośćformułzdaniowych(bezzmiennych wolnych). Interpretacjęprzypisującądanejformulewartośćprawdylogicznejnazywamy interpretacjąspełniającą,albomodelemtejformuły. Metodyopartenalogice—semantykarachunkupredykatów16

S p e łn ia ln o ść

Formułęnazywamyspełnialną,jeśliistniejeinterpretacjaspełniająca,czyli przypisującajejwartośćprawdylogicznej(inaczej:jeśliistniejemodeltejformuły). Formułajestniespełnialna,jeślinieistniejeżadnaspełniającająinterpretacja (model).Zkolei,jeśliformułamawartośćprawdydlakażdejmożliwejinterpretacji,to nazywamyjątautologią,alboformułąprawdziwą. Rozważmyprzykłady: At(Wumpus,2,2) ∃x,yAt(Gold,x,y) ∀x,y[At(Wumpus,x,y)∧At(Agent,x,y)]⇒AgentDead Wszystkiepodaneformułysąspełnialne,ponieważbeztrudumożemystworzyćsobie instancjęświatawumpusa,wktórejbędązachodziłypodanefakty.Jednakżadnanie jesttautologią.Coprawdaostatniedwieformułysąprawdziwewkażdejinstancji rozgrywkizgodnejzprawamiświatawumpusa.Jednakbeztrudumożemywymyślić inny,podobnyświat,gdzieniebędąoneobowiązywały. Przykłademtautologiimożebyćznaczniemniejinteresująca,chociaż zmatematycznegopunktuwidzeniafascynującaformuła:P∨¬P,gdziePjest dowolnym0-argumentowympredykatem,czylistwierdzeniemdowolnegofaktu. Metodyopartenalogice—semantykarachunkupredykatów17

K ró tk ie p o d su m o w a n ie — p yt a n ia sp ra w d za ją ce

1.Dlapodanychponiżejformułrachunkupredykatówodpowiedz,czydanaformuła jest:spełnialna,niespełnialna,tautologią. (a)P (b)P(x) (c)∀xP(x) (d)∃xP(x) (e)[P⇒Q]∧P∧¬Q (f)[P⇒Q]⇔[¬P∨Q] Metodyopartenalogice—semantykarachunkupredykatów18

W yn ik a n ie lo g ic zn e

Wwielusytuacjachagentchciałbyprzeprowadzićjakieśwnioskowanie.Naprzykład: wcelustwierdzeniazachodzeniafaktów,októrychagentniemainformacji,alektóre mogąwynikaćzinnychinformacji,któreagentposiada.Takieprzypadkiwidzieliśmyna przykładachzeświatawumpusa.Innąsytuacjągdyagentmógłbychciećwyciągać wnioskijestpróbaokreśleniamożliwychskutkówswoichdziałań—pożądanychbądź niepożądanych. Chcemymiećmożliwośćefektywnegosprawdzania,czyjednefaktywynikajązinnych. Jednaklogikapozwalajedynieokreślaćwynikanieformuł. Wynikanielogiczneformułyϕzezbioruformuł∆zachodzi,gdykażdainterpretacja spełniającawszystkieformułyz∆spełniateżformułęϕ,cozapisujemy: ∆|=ϕ Dlaczegowłaśnietakdefiniujemywynikanie?Bochcemymiećuniwersalnyaparat logiczny,prowadzącyprocesywnioskowaniapoprawnedlawszystkichmożliwych interpretacji.Ponieważoperujemynaformułach,chcemymiećpewność,żeproces wnioskowaniajestsłusznyrównieżdlakonkretnejdziedzinyproblemowej,zktórama doczynieniaagent. Metodyopartenalogice—wnioskowanie19

D yg re sj a — ra ch u n e k zd a ń

Wlogiceistniejejęzykprostszyodrachunkupredykatówzwanyrachunkiemzdań. Nieistniejąwnimtermy,zatempredykatyograniczonesądopredykatów 0-argumentowych,zwanychzdaniami.Formułyatomowestanowiąpojedynczesymbole zdaniowe,aformułyzłożonemożnabudowaćzapomocąspójników,podobniejak wrachunkupredykatów.Kwantyfikatorówniema. Semantykarachunkuzdańjestbardzouproszczona.Zamiastrozpatrywaćwszystkie możliweinterpretacjedanejformuływystarczypodzielićjenagrupy,wktórych poszczególnesymbolezdaniowesąprawdziwelubnieprawdziwe.Wefekcie,zamiast rozpatrywaćinterpretacje,możnabadaćwszystkiemożliwekombinacjeprawdyifałszu symbolizdaniowych.Prostąprocedurątakiegobadaniajestbudowanietabelek zerojedynkowych. Wrachunkupredykatówniejesttomożliwe,ponieważwartośćlogicznaformułyzależy odwartościtermów,któresąargumentamipredykatów.Niestety,rachunekzdańjest zbytsłaby(mówimy:niedostatecznieekspresyjny)dlazastosowańpraktycznych. Metodyopartenalogice—wnioskowanie20

R e g u ły w n io sk o w a n ia

Sprawdzaniewynikaniaprzezinterpretacjeiniespełnialnośćmożebyćuciążliwe.Jestto spowodowanekoniecznościąuwzględnieniawszystkichmożliwychinterpretacji,których możebyćbardzodużo. Zamiastsprawdzaniawynikanialogicznego,wlogicestosujesiępodejściezwane dowodzeniemtwierdzeń.Wprowadzasięreguływnioskowania,którepozwalają zjednychformułtworzyćinnezapomocąsyntaktycznychprzekształceń. Naprzykład,jednazpodstawowychregułwnioskowaniazwanamodusponens,albo regułąodrywania,mapostać: ϕ,ϕ⇒ψ ψ Wprzypadkugdybyagentposiadałfakty:SuszaiSusza⇒NiskiePlony,to podstawiającjedopowyższegoschematumiałbyprawowywieśćnowyfakt: NiskiePlony. Metodyopartenalogice—wnioskowanie21

D o w o d ze n ie tw ie rd ze ń

Dowodemformułyϕdlazbioruformuł∆,zwanegozbioremaksjomatów, nazywamyciągformuł,zktórychostatniąformułąjestϕ,azktórychkażdaspełnia jedenzwarunków: 1.jesttautologią, 2.jestjednymzaksjomatów, 3.jestformułąotrzymanązformułpoprzedzającychjąwdowodzie(leżącychbardziej nalewo)zapomocąjednejzposiadanychregułwnioskowania. Twierdzeniemzbioruformuł∆nazywamykażdąformułęϕktóraposiadadowóddla zbioru∆.Wtedymówimy,żeformułęϕmożnawywieśćzezbioruaksjomatów∆,co zapisujemy: ∆⊢ϕ Zbiórwszystkichtwierdzeńzbioruformuł∆nazywamyteoriątegozbioruioznaczamy T(∆). Metodyopartenalogice—wnioskowanie22

W n io sk o w a n ie p rz e z d o w o d ze n ie tw ie rd ze ń

Początkowowprowadziliśmywynikanielogiczne(∆|=ϕ)jakometodęwnioskowania, tzn.stwierdzaniawynikaniafaktów.Jednakbrakbyłowygodnejproceduryefektywnego obliczaniategowynikania. Dowodzenietwierdzeń(∆⊢ϕ)oferujepotencjalniedobrąproceduręwnioskowaniadla agentaposługującegosięlogikąjakojęzykiemreprezentacji.Chcącwywieśćjakiś pożądanyfaktzezbioruaksjomatówmożnawnajgorszymprzypadkusystematycznie generowaćwszystkiemożliweskończoneciągiformułspełniającychdefinicjędowodu tegofaktu.JeśliistniejedowódodługościN,towtejprocedurzezostanieon wygenerowany.Tojużlepiejniżsprawdzaniewszystkichinterpretacji,którenawet trudnosobiewyobrazić. Jednakczydowodzenietwierdzeńjestrówniedobrąmetodąsprawdzaniawynikania faktów,którezachodząwrzeczywistejdziedzinieproblemowej? Niejesttowcaleoczywiste. Metodyopartenalogice—wnioskowanie23

S ys te m y d o w o d ze n ia tw ie rd ze ń

Wlogicezdefiniowanoszeregsystemówdowodzeniatwierdzeńwprowadzających różnezestawyregułwnioskowania,atakżepewneformułypoczątkowe,któremożna wnichstosować(aksjomaty).Wtymwykładzieniebędziemyzagłębiaćsię wkonstrukcjętychsystemów,jednakmusimyznaćirozumiećpewneichwłasności. Reguławnioskowaniajestpoprawnajeślimożnazajejpomocąwywieśćfałszjedynie zniespełnialnegozbioruprzesłanek. Zbiórregułwnioskowaniajestkompletnyjeślimożnazjegopomocąwywieśćfałsz zkażdegoniespełnianegozbioruprzesłanek. Systemdowodzeniatwierdzeńjestpełnyjeślijestpoprawnyikompletny.Wtakim systemiezezbioruprzesłanekmożnawywieśćfałszwtedyitylkowtedygdyzbiórten jestniespełnialny(podwarunkiem,żesątoformułyzamknięte). Awięctocobyłobypotrzebneagentowiinteligentnemu,tojestpełnysystem dowodzeniatwierdzeń,zefektywnąobliczeniowoprocedurądowodową. Metodyopartenalogice—wnioskowanie24

K ró tk ie p o d su m o w a n ie — p yt a n ia sp ra w d za ją ce

1.Wyjaśnijdlaczegownioskowanieagentaojegoświeciepowinnobyćoparte owynikanielogiczne. 2.Naczympolegadowodzenietwierdzeńijakąrolępełniąwnimreguły wnioskowania? 3.Kiedymożemyzastosowaćdowodzenietwierdzeńwceluwnioskowania owłasnościachzachodzącychwjakiejśdziedzinieproblemowej? 4.Odpowiedzczyzachodząponiższewłasności(wprzypadkudowodliwości⊢przyjmij, żejedynąmożliwąregułądowodzeniajestmodusponens:ϕ,ϕ⇒ψ ψ): {P,P⇒Q}|=P{P,P⇒Q}⊢P {P,P⇒Q}|=Q{P,P⇒Q}⊢Q {P,P⇒Q}|=P∧Q{P,P⇒Q}⊢P∧Q Niejestkonieczneprzeprowadzenieformalnegodowodukażdegozpowyższych przypadków,wystarczypółformalnesłowneuzasadnienie. Metodyopartenalogice—wnioskowanie25 Metodyopartenalogice—wnioskowanie26

P o st a ć d ys ju n k cy jn a n o rm a ln a (D N F )

Proceduryautomatycznegoprzetwarzaniaformułlogicznychwymagajązapisywania formułwpewnychstandardowychpostaciachnormalnych. Formułyatomoweiichnegacjenazywamyliterałami,np.:P,¬Q(x,f(a)). FormułajestwpostaciDNF(DisjunctiveNormalForm)jeślijestalternatywą koniunkcjiliterałów.Zarównoalternatywęjakikoniunkcjętraktujemytutajjako spójnikin-arne,dladowolnegon,niekonieczniebinarne,korzystajączichłączności. DlakażdejformułylogicznejistniejerównoważnajejlogicznieformuławpostaciDNF. Naprzykład,formuła(¬P∧Q)∨RjestjużwpostaciDNF,natomiastformułę ¬P∧(Q∨R)możnaprzekształcićdopostaciDNFkorzystajączrozdzielności koniunkcjiwzględemalternatywy:(¬P∧Q)∨(¬P∧R). PrzekształcenieformułydopostaciDNFniejestjednoznaczne;możeistniećwiele formułwpostaciDNFrównoważnychdanejformule. Metodyopartenalogice—postacinormalneformuł27

P rz e k sz ta łc a n ie fo rm u ł d o D N F

JednąszczególnąkonstrukcjępostaciDNFmożnaotrzymaćzzerojedynkowejtabelki definiującejprawdziwośćformuływzależnościodprawdziwościwchodzącychwjej składformułatomowych. Przykład: (P⇒Q)∧(Q⇒P) PQP⇒QQ⇒P(P⇒Q)∧(Q⇒P) 00111 01100 10010 11111 Wybierającwierszetabeli,dlaktórychformułamawartośćprawdy(jedynkawostatniej kolumnie),konstruujemyformułęwpostaciDNF: (¬P∧¬Q)∨(P∧Q) Metodyopartenalogice—postacinormalneformuł28

P o st a ć k o n iu n k cy jn a n o rm a ln a (C N F )

Oformule,którajestkoniunkcjąalternatywliterałówmówimy,żejestwpostaciCNF (ConjunctiveNormalForm).Formuły,którasąalternatywamiliterałównazywamy klauzulami.ZatemformuławpostaciCNFjestkoniunkcjąklauzul.(Dlategoskrót CNFbywarównieżrozwijanyjakoClausalNormalForm). PrzykładformuływpostaciCNF:(P∨Q∨¬R)∧(P∨¬Q∨R).CNFjest analogiczną,dualnądopostaciDNFformązapisuformuł.Możeonapoczątkowo wydawaćsięmniejintuicyjna,jestjednakznaczniebardziejprzydatnawsystemach automatycznegodowodzeniatwierdzeń. Naprzykład,postaćCNFjestmodularna,tzn.gdychcemydodaćdoposiadanej formuływpostaciCNFjakiśnowyfaktwpostaciinnejformułyCNF,tooperacjata jesttrywialnainienaruszapostacidotychczasposiadanejformuły,wodróżnieniuod DNF. Metodyopartenalogice—postacinormalneformuł29

P rz e k sz ta łc a n ie fo rm u ł d o C N F

Rozważmyponownieprzykładowąformułęijejzerojedynkowątabelęprawdy: (P⇒Q)∧(Q⇒P) PQP⇒QQ⇒P(P⇒Q)∧(Q⇒P) 00111 01100 10010 11111 AnalogiczniedoalgorytmukonstrukcjipostacikanonicznejDNFformuły,możemy skonstruowaćpostaćCNFbiorącwierszezzerowąwartościąformuły,ikonstruując klauzuleeliminującetewiersze: (¬P∨Q)∧(P∨¬Q) Metodyopartenalogice—postacinormalneformuł30

P u st e k o n iu n k cj e i p u st e k la u zu le

Możemymówićopojedynczychliterałachjakoo1-arnych(unarnych)koniunkcjach klauzul,alboklauzulach(alternatywachliterałów).Cowięcej,dopuszczamyrównież klauzule,orazkoniunkcjeklauzul,0-arne,czylipuste. p1∧p2∧...∧pn=∧(p1,p2,...,pn)p1∨p2∨...∨pn=∨(p1,p2,...,pn) p∧q=∧(p,q)p∨q=∨(p,q) p=∧(p)p=∨(p) ␣=∧()␣=∨() Zauważmy,żeoileprawdziwośćniepustychkoniunkcjilubklauzulzależyod prawdziwościichelementów,topustekoniunkcjeorazklauzulepowinnymiećjakąś stałąinterpretacjęlogiczną.Przezprosteuogólnieniedefinicjiprawdziwościspójników możemyotrzymaćfakt,żepustakoniunkcjajestformułąprawdziwą(tautologią), natomiastpustaklauzulajestformułąfałszywą(niespełnialną). Przyzapisieformułlogicznychwpostacizbiorówlublist,pustekoniunkcjeiklauzule pojawiająsięjakozbiorypuste{}lubpustelisty:()orazNIL.Dodatkowostosujesię symbol✷dlazapisupustejklauzuliwnotacjilogicznej. Metodyopartenalogice—postacinormalneformuł31 Przykład: Weźmyformułę(P∧Q)zapisanąwpostacizbioruklauzul(jednoliterałowych): {P,Q}.Dodaniedotegozbiorukoniunkcjipustej:{P,Q}∪{}odpowiadawnotacji logicznejoperacji:(P∧Q)∧T≡(P∧Q)(gdzieTsymbolizujeprawdę).Potwierdza tosłusznośćinterpretacjipustejkoniunkcjijakotautologii. Analogicznie,możemyzapisaćklauzulę(P∨Q)wpostacizbioruliterałów:{P,Q}. Dodaniedotegozbioruklauzulipustej:{P,Q}∪{}odpowiadawnotacjilogicznej operacji:(P∨Q)∨F≡(P∨Q)(gdzieFsymbolizujefałsz).Takwięcrównież interpretacjapustejklauzulijakoformułyfałszywejjestpoprawna. Metodyopartenalogice—postacinormalneformuł32

P rz e k sz ta łc a n ie fo rm u ł lo g ic zn yc h d o p o st a ci k la u zu lo w e j

Formułębezzmiennychwolnychmożemyprzekształcićdopostaciklauzulowej (inaczej:prenex)gdziewszystkiekwantyfikatoryzapisanesąprzedformułą: (i)przemianujzmiennezwiązanekwantyfikatoraminaunikalne, (ii)zastąpkoniunkcjamiialternatywamipozostałespójnikilogiczne, (iii)przesuńnegacjedowewnątrzformuł(dosymbolipredykatów), (iv)wyodrębnijkwantyfikatorypozaformułę, (v)przekształćformułędopostacikoniunkcyjnej(CNF), (vi)zastąpwszystkiekwantyfikatoryegzystencjalnefunkcjamiSkolema. Pierwszepięćkrokówsąrównoważnościowymiprzekształceniamilogicznymi(przy zachowaniuwłaściwejkolejnościwyodrębnianychkwantyfikatorówwkroku(iv)).Krok (vi),tzw.skolemizacja,poleganazastąpieniuformułpostaci: ∀x1∀x2...∀xn∃yΦ(x1,x2,...,xn,y) formułą ∀x1∀x2...∀xnΦ(x1,x2,...,xn,fy(x1,x2,...,xn)) gdziefyjestnowowprowadzonymsymbolemfunkcyjnymzwanymfunkcjąSkolema. (Wprzypadkubrakukwantyfikatorów∀będzietostałaSkolema.) Metodyopartenalogice—postacinormalneformuł33

T w ie rd ze n ie S k o le m a

Ostatnikrokwalgorytmieprzekształceniaformułydopostaciklauzulowejniejest równoważnościowymprzekształceniemlogicznym.Toznaczy,dlaoryginalnejformuły logicznejΦ,iotrzymanejwwynikuprzekształceniajejpostaciklauzulowejΦ′ , wogólnościΦ6≡Φ′. Zachodzijednaknastępującawłasność,zwanatwierdzeniemSkolema:dla zamkniętejformułyΦ,jeśliΦ′jestjejpostaciąklauzulową,toΦjestspełnialnawtedy itylkowtedygdyΦ′ jestspełnialna. Zatem,oileniemożemywogólnościposługiwaćsiępostaciąklauzulowąΦ′zamiast oryginalnejformułyΦ,tojednakmożemyposługiwaćsiętąpostacią dlacelówdowodzeniaspełnialności(lubniespełnialności). Istniejeniezwykleprzydatnyschematwnioskowania,wykorzystującyformuływpostaci klauzulowej,zapisywaneczęstowpostacizbioru(lublisty)klauzul,gdzieposzczególne klauzulesązapisanewpostacizbiorów(lublist)literałów. Metodyopartenalogice—postacinormalneformuł34

K ró tk ie p o d su m o w a n ie — p yt a n ia sp ra w d za ją ce

Przekształćdopostaciprenexnastępująceformułyrachunkupredykatów: 1.∀x[(P(x)⇒Q(x))∧(P(x)⇒R(x))] 2.∀x[(P(x)∧Q(x))∨(R(x)∧S(x))] 3.∀x∃y[P(x)⇒Q(x,y)] 4.∃x∀y[P(x,y)⇒Q(A,x)] 5.∀x∃y[P(x,y)⇒Q(y,f(y))] Metodyopartenalogice—postacinormalneformuł35 Metodyopartenalogice—postacinormalneformuł36

R e zo lu cj a — p rz yp a d e k k la u zu l p o d st aw io n yc h

Rezolucjadladwóchklauzulpodstawionych:gdyistniejewspólnyliterałmający wdwóchklauzulachprzeciwneznaki,torezolucjatworzynowąklauzulę,zwaną rezolwentą,będącąpołączeniemoryginalnychdwóchklauzulzwyłączeniem wspólnegoliterału. Rozważmyprzykład,dlaklauzul: P∨Q(A)oraz¬S∨¬Q(A) rezolucjautworzyrezolwentęP∨¬S. Zauważmy,żedlaparklauzul:(P∨Q(A)),(¬S∨Q(A))jakrównieżdla: (P∨Q(A)),(¬S∨¬Q(B))nieistniejąwspólneliterałyoprzeciwnychznakach, zatemwykonanierezolucjidlatychparklauzulniejestmożliwe. Fakt:rezolwentazawszewynikalogiczniezpołączenia(koniunkcji)klauzul wyjściowych,zatemjakoreguławnioskowaniarezolucjajestpoprawna(sound). Metodyopartenalogice—rezolucja37 Ciekaweprzypadkiszczególnerezolucji(symbol❀oznaczatumożliwośćwykonania rezolucjiiotrzymaniawskazanegowyniku): Poraz¬P∨Q❀Qmodusponens P∨Qoraz¬P∨Q❀Qmocniejszawersja P∨Qoraz¬P∨¬Q❀P∨¬Ptautologia P∨Qoraz¬P∨¬Q❀Q∨¬Q-”- Poraz¬P❀NILsprzeczność ¬P∨Qoraz¬Q∨R❀¬P∨Rprzechodniość (P⇒Q)(Q⇒R)(P⇒R)implikacji Metodyopartenalogice—rezolucja38

K ró tk ie p o d su m o w a n ie — p yt a n ia sp ra w d za ją ce

Dlaponiższychzbiorówformuł,zapiszwszystkiemożliwedootrzymaniarezolwenty. Jeśliniejestmożliwewykonanierezolucji,towyjaśnijdlaczegonie.Porównaj otrzymanerezolwentyzwnioskamilogicznymi,któremożeszwyciągnąćintuicyjnie zpodanychformuł. Zwróćuwagęnaprzecinki,abyprawidłowoodczytaćformuływzbiorach. 1.{P∨Q∨R,¬P∨¬Q∨¬R} 2.{P∨Q,P∨¬Q,¬P∨Q} 3.{P⇒(Q∨R),¬Q∧¬R} 4.{P⇒Q,R⇒Q,P∨R} Metodyopartenalogice—rezolucja39 Metodyopartenalogice—rezolucja40

P o d st aw ie n ia zm ie n n yc h w fo rm u ła ch

Będziemyrozważaliprzekształceniaformułpolegającenazastępowaniuzmiennych wformułachinnymiwyrażeniami(termami).Ponieważzmiennewformułachwpostaci prenexdomyślniezwiązanesąkwantyfikatoramiuniwersalnymi,zastępowanie zmiennychinnymitermamioznaczabranieszczególnychprzypadkówformuły. Podstawieniem(substitution)nazwiemyzbiórodwzorowańokreślającychtermy podstawianepodposzczególnezmienne.Podstawianetermyniemogązawierać zastępowanejzmiennej.Przykładpodstawienia:s={x7→A,y7→f(z)}. Wykonaniepodstawieniapoleganasyntaktycznymzastąpieniuwszystkich wystąpieńdanejzmiennejwformulezwiązanymzniątermem.Wszystkiezastąpienia wykonywanesąjednocześnie,czyliwynikiemwykonaniapodstawienia s={x7→y,y7→A}natermief(x,y)będzietermf(y,A). Zauważ,żewtensposóbniemaznaczeniawjakiejkolejnościzmiennesązastępowane, pomimoiżpodstawieniejestzbiorem(nieuporządkowanym). Metodyopartenalogice—unifikacja41 Złożeniempodstawieńs1is2(zapisywanym:s1s2)nazwiemypodstawienieuzyskane przezzastosowaniepodstawienias2dotermówzs1,orazdopisaniedootrzymanego zbioruwszystkichparzs2zezmiennyminiewystępującymiws1. Φs1s2=(Φs1)s2 s1(s2s3)=(s1s2)s3 Metodyopartenalogice—unifikacja42

U n ifi k a cj a

Unifikacjąnazywamytakiepodstawienietermówpodzmiennewzbiorzeformuł,aby sprowadzićwszystkieformuływzbiorzedoidentycznych(lubrównoważnychlogicznie, patrzwyjaśnienieniżej)formuł,czylizbiorusingletonowego. Unifikatorzbioruformułtojestpodstawienieredukującezbiórdo jednoelementowego.Zbiórjestunifikowalnyjeśliistniejejegounifikator. Naprzykład:zbiór{P(x),P(A)}jestunifikowalny,ijegounifikatoremjest s={x7→A}. Podobnie,zbiór{P(x),P(y),P(A)}jestunifikowalny,ajegounifikatoremjest s={x7→A,y7→A}. Zbiór{P(A),P(B)}niejestunifikowalny,podobniejakzbiór{P(A),Q(x)}. Metodyopartenalogice—unifikacja43

U n ifi k a cj a (c d .)

Unifikacjajestogólnąprocedurą,aletutajbędziemywykonywaćunifikacjewyłącznie nazbiorachklauzul.Rozważmyponiższe,przykładowezbioryklauzul: Φ={P∨Q(x),P∨Q(A),P∨Q(y)} Ψ={P∨Q(x),P∨Q(A),P∨Q(f(y))} Ω={P∨Q(x),P∨Q(A)∨Q(y)} ZbiórΦjestunifikowalny,jegounifikatoremjests={x7→A,y7→A}, azunifikowanymzbioremjestsingletonowyzbiórΦs={P∨Q(A)}. ZbiórΨniejestunifikowalny. ZbiórΩjestbardziejskomplikowanymprzypadkiem.Stosującczystosyntaktyczną unifikację,niejestonunifikowalny,bopowykonaniusamegopodstawieniaformuły niesąidentyczne.Jednakstosującsemantycznąunifikację,jestonunifikowalny, ponieważpowykonaniupodstawieniaformułysąlogicznierównoważne.Będziemy dopuszczaliunifikacjęsemantycznązzastosowaniemłącznościiprzemienności alternatywy. Metodyopartenalogice—unifikacja44

N a jo g ó ln ie js zy u n ifi k a to r (m g u )

Najogólniejszymunifikatoremunifikowalnegozbioruformuł,albomgu(most generalunifier),nazywamynajprostszy(minimalny)unifikatordlategozbioru. Dlaunifikowalnegozbioruformułzawszeistniejejegomgu,adowolnyunifikatordla tegozbiorumożnaotrzymaćprzezzłożeniemguzjakimśinnympodstawieniem. Algorytmunifikacjipozwalawyznaczyćmguzbioruformuł. Metodyopartenalogice—unifikacja45

K ró tk ie p o d su m o w a n ie — p yt a n ia sp ra w d za ją ce

Dlaponiższychzbiorówklauzulodpowiedz,czydanyzbiórjestunifikowalny.Jeślitak, topodajjegounifikator.Spróbujpodaćzarównomgu,jakiinnyunifikator,którynie jestmgu.Jeślizbiórniejestunifikowalny,tokrótkouzasadnijdlaczego. Zwróćuwagęnaprzecinki,abyprawidłowoodczytaćformuływzbiorach. 1.{P(x),P(f(x))} 2.{P(x,y),P(y,x)} 3.{P(x,y),P(y,f(x))} 4.{P(x,y),P(y,f(y))} 5.{P(x,y),P(y,z),P(z,A)} Metodyopartenalogice—unifikacja46

R e zo lu cj a — p rz yp a d e k o g ó ln y

Rezolucjawogólnymprzypadku:gdydladwóchklauzul(zbiorówliterałów){Li} i{Mi}istniejąichpodzbiory{li}i{mi},zwaneliterałamikolidującymi,takie,że zbiór{li}∪{¬mi}dajesięzunifikowaćisjestjegomgu,wtedyichrezolwentąjest zbiór[{Li}−{li}]s∪[{Mi}−{mi}]s. Mogąistniećróżnerezolwentydanychklauzuldlaróżnychwyborówpodzbiorówich literałów.Naprzykład,rozważmynastępująceklauzule: P[x,f(A)]∨P[x,f(y)]∨Q(y)oraz¬P[z,f(A)]∨¬Q(z) Wybierając{li}={P[x,f(A)]}oraz{mi}={¬P[z,f(A)]}otrzymujemy rezolwentę: P[z,f(y)]∨¬Q(z)∨Q(y) Natomiastwybierając{li}={P[x,f(A)],P[x,f(y)]}oraz{mi}={¬P[z,f(A)]} otrzymujemy: Q(A)∨¬Q(z) Metodyopartenalogice—rezolucja47

K ró tk ie p o d su m o w a n ie — p yt a n ia sp ra w d za ją ce

Dlaponiższychzbiorówklauzul,zapiszwszystkiemożliwedootrzymaniarezolwenty. Dlakażdejrezolwentyzanotuj,zktórychklauzulzostałaotrzymana,ijakiebyło zastosowanepodstawienie.Jeśliniejestmożliwewykonanierezolucji,towyjaśnij dlaczegonie. Zwróćuwagęnaprzecinki,abyprawidłowoodczytaćformuływzbiorach. 1.{¬P(x)∨Q(x),P(A)} 2.{¬P(x)∨Q(x),¬Q(x)} 3.{¬P(x)∨Q(x),P(f(x)),¬Q(x)} Metodyopartenalogice—rezolucja48

R e zo lu cj a ja k o re g u ła w n io sk o w a n ia

Rezolucjajestpoprawnąregułąwnioskowaniaponieważklauzulaotrzymanazpary klauzulwwynikuzastosowaniarezolucji,wynikaznichlogicznie.Jednakniejest kompletna,toznaczyniemożemyzjejpomocąwygenerowaćzdanejformuły∆ każdegownioskuϕ,takiegoże∆⊢ϕ. Naprzykład,dla∆={P,Q}niemożemyrezolucjąwywieśćformułP∨QaniP∧Q, adla∆={∀xR(x)}niemożemywywieśćformuły∃xR(x). Jednakjeślizastosujemyrezolucjęwprocedurzedowodzenianiewprost,czyliprzez zaprzeczenietezyiwyprowadzeniesprzeczności,reprezentowanejprzezklauzulępustą (oznaczaną✷),tomożemyudowodnićniąkażdetwierdzenie.Zatemwtymsensie rezolucjajestkompletna(refutationcomplete). Rozważmypowyższeprzykłady.Dla∆={P,Q}zaprzeczeniemformułyP∨Qsą klauzule¬Pi¬Qikażdaznichpozwalanatychmiastwygenerowaćklauzulępustą zodpowiedniąklauzuląz∆.ZaprzeczeniemformułyP∧Qjestklauzula¬P∨¬Q imożemyuzyskaćklauzulępustąwdwóchkrokachrezolucji.Dla∆={∀xR(x)} zaprzeczeniemformuły∃xR(x)jest¬R(y),któraunifikujesięzklauzuląR(x) otrzymanąz∆idajeklauzulępustąwjednymkrokurezolucji. Metodyopartenalogice—rezolucja49

D o w o d ze n ie tw ie rd ze ń o p ar te n a re zo lu cj i

Podstawowyschematwnioskowaniaopartegonarezolucji,gdyposiadamyzbiór aksjomatów∆ichcemyzniegowywieśćformułęϕ,jestnastępujący.Łączymyzbiory klauzulotrzymanychz∆i¬ϕ,ipróbujemywywieśćsprzeczność(klauzulępustą) zotrzymanegołącznegozbioruklauzul,przezzastosowanierezolucjinakolejnych parachwybranychklauzul.Wtymprocesieuzyskanawbieżącymkrokurezolucjinowa klauzulazostajekażdorazowodołączonadogłównegozbioruklauzul,iprocedurajest powtarzana. Podstawowywyniklogikimatematycznejtuwykorzystywanyjestnastępujący.Jeśli uruchomimyrezolucjęnazbiorzeklauzulotrzymanymzniespełnialnejformuły, zjakimśsystematycznymalgorytmemgenerowaniarezolwent,towpewnymmomencie otrzymamyklauzulępustą.Inaodwrót,jeślizezbioruklauzulotrzymanegozjakiejś formułymożnaprocedurąrezolucjiwygenerowaćklauzulępustą,totenzbiórklauzul, aletakżeoryginalnaformuła,sąniespełnialne.Obejmujetorównieżklauzuleotrzymane wwynikuskolemizacji,awięcjestzarazempotwierdzeniempoprawnościtejprocedury. Metodyopartenalogice—rezolucja50

D o w o d ze n ie tw ie rd ze ń : p rz yk ła d

Wiadomo,że: 1.Ktopotraficzytaćtenjestoświecony.(∀x)[R(x)⇒L(x)] 2.Delfinyniesąoświecone.(∀x)[D(x)⇒¬L(x)] 3.Niektóredelfinysąinteligentne.(∃x)[D(x)∧I(x)] Należyudowodnićtwierdzenie: 4.Sątacyinteligentniconiepotrafiączytać.(∃x)[I(x)∧¬R(x)] PokonwersjidopostaciprenexCNFotrzymujemyklauzule: C1:¬R(u)∨L(u)zpierwszegoaksjomatu C2:¬D(v)∨¬L(v)zdrugiegoaksjomatu C3a:D(A)ztrzeciegoaksjomatu,cz.1 C3b:I(A)ztrzeciegoaksjomatu,cz.2 NT:¬I(w)∨R(w)znegacjitwierdzenia Zkolejnychkrokówrezolucjiotrzymujemy: C5:R(A)rezolwentaklauzulC3biNT C6:L(A)rezolwentaklauzulC5iC1 C7:¬D(A)rezolwentaklauzulC6iC2 C8:✷rezolwentaklauzulC7iC3a

C3aC2C1C3bNT

❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊❊

❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊

w=A

❊ ❊ ❊ ❊ ❊ ❊ ❊ ❊u=A ❊ ❊

❉ ❉ ❉ ❉ ❉

v=A

✂ ✂ ✂ ✂✂

C5

✂ ✂ ✂ ✂✂

C6

✂ ✂ ✂ ✂✂

C7

✂ ✂ ✂ ✂✂

C8=✷ Metodyopartenalogice—rezolucja51 Metodyopartenalogice—rezolucja52

D o w o d ze n ie tw ie rd ze ń : p o w a żn ie js zy p rz yk ła d

Rozważmyprzykładzmatematyki.2Chcemyudowodnić,żeprzekrójdwóchzbiorów zawierasięwdowolnymznich.Zaczynamyodwypisaniaaksjomatów,zktórych rozumowaniebędziemusiałokorzystać.Wtymprzypadkusątodefinicjepojęć przekrojuizawieraniasięzbiorów. ∀x∀s∀t(x∈s∧x∈t)⇔x∈s∩t ∀s∀t(∀xx∈s⇒x∈t)⇔s⊆t Formuładoudowodnienia: ∀s∀ts∩t⊆s 2PrzykładzapożyczonyzksiążkiGeneserethaiNilssona„LogicalFoundationsofArtificialIntelligence”. Metodyopartenalogice—rezolucja53 Poprzetworzeniudopostaciklauzulotrzymujemy: 1.{x6∈s,x6∈t,x∈s∩t}zdefinicjiprzekroju 2.{x6∈s∩t,x∈s}zdefinicjiprzekroju 3.{x6∈s∩t,x∈t}zdefinicjiprzekroju 4.{F(s,t)∈s,s⊆t}zdefinicjizawieraniasię 5.{F(s,t)6∈t,s⊆t}zdefinicjizawieraniasię 6.{A∩B6⊆A}zzaprzeczeniatezy ZauważmyfunkcjeSkolemawklauzulach4i5,orazstałeSkolemawklauzuli6.Dalej następujewywódprowadzącydosyćprostodoklauzulipustej. 7.{F(A∩B,A)∈A∩B}zklauzul4.i6. 8.{F(A∩B,A)6∈A}zklauzul5.i6. 9.{F(A∩B,A)∈A}zklauzul2.i7. 10.{}zklauzul8.i9. Tokoniecdowodu.Celosiągnięty.Trochętrudnopoczućsatysfakcjęjakazwykle towarzyszyosiągnięciutradycyjnegodowodumatematycznego.Równieżabyprześledzić rozumowanieinp.jesprawdzić,trzebasiętrochęnapracować,aczkolwiekwprzypadku tegodowodujesttojeszczewzględnieproste. Metodyopartenalogice—rezolucja54

K ró tk ie p o d su m o w a n ie — p yt a n ia sp ra w d za ją ce

Dlapodanychponiżejzbiorówaksjomatów∆iformułyϕ,spróbujudowodnić∆⊢ϕ metodąrezolucjiniewprost.Zacznijodzaprzeczeniaformułycelowej,następnie zotrzymanegozaprzeczeniaizbioruaksjomatówutwórzpodstawowyzbiórklauzul. 1.∆={∀x(Lubi(x,Wino)⇒Lubi(Rychu,x)),Lubi(Zdzich,Wino)} ϕ=Lubi(Rychu,Zdzich) 2.∆={∀x(Lubi(x,Rychu)⇒Lubi(Rychu,x)),¬Lubi(zona(Zdzich),Rychu)} ϕ=Lubi(Rychu,zona(Zdzich)) 3.∆={∀x(Lubi(x,Wino)⇒Lubi(Rychu,x)),Lubi(Zdzich,Wino)} ϕ=(Lubi(Rychu,Zdzich)∨Lubi(Rychu,zona(Zdzich)) 4.∆={∀x(Lubi(x,Wino)⇒Lubi(Rychu,x)),Lubi(Zdzich,Wino)} ϕ=(Lubi(Rychu,Zdzich)∧Lubi(Rychu,zona(Zdzich)) Metodyopartenalogice—rezolucja55 Metodyopartenalogice—rezolucja56