John McCarthy cikke a „Programs with Common Sense” (McCarthy, 1958, 1968) tette híressé az ágens fogalmát, egy olyan programét, amely az érzetek és cselekvések összekapcsolására logikai következtetést használ. A cikk kitűzte a deklarativizmus zászlóját, megmutatva, hogy szoftverek írásának igen elegáns módszere az, ha a szükséges ismereteket közöljük az ágenssel. Allen Newell cikke (1982) a „The Knowledge Level” tárgyalja azt a megközelítést, hogy racionális ágensek leírhatók és elemezhetők egy absztrakt szinten, ami az általuk birtokolt tudást és nem azt a programot definiálja, amit futtatnak. A mesterséges intelligencia deklaratív és procedurális megközelítéseit hasonlítja össze Boden (Boden, 1977). A vitát, mások mellett Brooks (Brooks, 1991) és Nilsson (Nilsson, 1991) írásai élesztették fel újra.

Magának a logikának az eredete az ősi görög filozófiában és matematikában található. Számos logikai alapelv – a mondatok szintaktikus struktúrájának összekötése az igaz vagy hamis jellegükkel, a jelentésükkel, a bennük megjelenő argumentumok érvényességével – elszórt helyeken megtalálható Platón műveiben. Arisztotelész készítette az első ismert, rendszerezett munkát a logikáról. Munkáját diákjai gyűjtötték össze halála után, i. e. 322-ben az Organon c. tanulmányban. Arisztotelész szillogizmusai (syllogisms) olyan logikai állítások voltak, amelyeket ma következtetési szabályoknak neveznénk. Habár a szillogizmus tartalmazott elemeket, mind a propozíciós, mind az elsőrendű logikából, a rendszer, mint egész, igen gyengének számít a modern kívánalmak szerint. Nem tette lehetővé tetszőleges komplexitású mondatok létrehozását a következtetési mintákban, mint a modern ítéletlogika.

A hasonló Megara és sztoikus iskolák (az i. e. 5. században indultak, és több száz éven keresztül működtek) vezették be az implikációt és más alapvető szerkezeteket, amelyeket ma is használunk a modern ítéletlogikában. Logikai összekötőjelek definiálására vezette be az igazságtábla használatát Philón és Megara. A sztoikusok öt alapvető következtetési szabályt használtak, amelyeket igazolás nélkül érvényesnek tartottak, köztük azt a szabályt, amelyet ma Modus Ponensnek nevezzünk. Számos szabályt vezettek le ebből az ötből, felhasználva többek között a dedukció elméletének alapelvét 7.5. szakasz - Az ítéletkalkulus következtetési mintái részben, és sokkal tisztábban használták a bizonyítás fogalmát, mint azt Arisztotelész tette. A sztoikusok azt állították, hogy az ő logikájuk teljes abban az értelemben, hogy tartalmaz minden érvényes következtetést, de ami fennmaradt munkájukból, az túlságosan töredékes ahhoz, hogy elemezhető legyen. A Megara és a sztoikus logikák történetének, már amennyire ezek ismertek, jó beszámolóját készítette el Benson Mates (Mates, 1953).

Wilhelm Leibniztől (1646–1716) származik a mesterséges formális nyelvi minták létrehozásának ötlete a logikai kapcsolatok tisztázásának és a logikai következtetés egy tisztán formális és mechanikus folyamattá való egyszerűsítése céljából. Leibniz saját matematikai logikája azonban igencsak tökéletlen volt, és rá inkább ezeknek a gondolatoknak mint célkitűzéseknek a bevezetéséért és nem e célok megvalósítására tett kísérletei miatt emlékezünk.

George Boole vezette be első igazán átfogó és működőképes formális logikai alapú rendszert a The Mathematical Analysis of Logic c. könyvében (Boole, 1847). Boole logikájának modellje közel állt a valós számok algebrájáéhoz, és elsődleges következtetési módszerként a logikailag ekvivalens mondatok helyettesítését használta. Bár Boole rendszere csak töredéke volt a teljes ítéletkalkulusnak, elég közel volt ahhoz, hogy a 19. század szerzői Boole-t követve hamar kitöltsék a hiányzó részeket. Schröder definiálta (Schröder, 1877) a konjunktív normál formát, míg a Horn-formát sokkal később Alfred Horn (Horn, 1951) vezette be. A modern ítéletkalkulus (és elsőrendű logika) első átfogó bemutatása Gottlob Frege Begriffschrift (Az írás fogalma vagy Fogalmi jelölés) c. könyvében (Frege, 1879) található.

Az első mechanikai eszközt, amely logikai következtetést végzett, Stanhope harmadik grófja (1753–1816) készítette. A Stanhope Demonstrator képes volt szillogizmusokat kezelni és bizonyos valószínűségi következtetéseket végezni. Wiliam Stanley Jevons – egyike azoknak, akik továbbfejlesztették és kiegészítették Boole munkáját – 1869-ben a Boole-logikán alapuló következtetések végrehajtására megépítette a „logical pianó”-ját. Ezeknek és más korai következtetésre készített mechanikus eszközöknek szórakoztató és tanulságos története Martin Gardner (Gardner, 1968) munkájában olvasható. Az első logikai következtetést végző, publikált számítógépes program a „Logic Theorist” volt, amelyet Newell, Shaw és Simon (Newell, Shaw és Simon, 1957) készítettek. Ezt a programot az emberi gondolkodás modellezésére szánták a szerzők. Bár Martin Davis (Davis, 1957) tervezett egy programot, ami bizonyíthatóan 1954-ben készült, de a Logic Theorist eredményeit korábban publikálták. Mind Davis 1954-es programja, mind a Logic Theorist részben ad hoc módszerekre épült, amelyek nem voltak jelentős hatással a későbbi automatikus dedukciós rendszerekre.

Az igazságtábláknak, mint az ítéletkalkulus nyelvében az érvényességnek vagy a mondat kielégíthetetlenségének a tesztjét egymástól függetlenül Ludwig Wittgenstein (1922) és Emil Post (1921) vezették be. A harmincas években jelentős haladást értek el az elsőrendű logika következtetési módszereinek terén. Nevezetesen, Gödel megmutatta (Gödel, 1930), hogy az elsőrendű logikában történő következtetésre egy teljes eljárást lehet kapni az ítéletlogikára történő redukcióval, felhasználva Herbrand elméletét (Herbrand, 1930). A 9. fejezetben újra áttekintjük ennek történetét, itt most a lényeges pont az, hogy a hatvanas években, a hatékony ítéletkalkulus algoritmusok fejlesztésében a matematikusok érdeklődését jelentős mértékben motiválta az a cél, hogy hatékony tételbizonyítót készítsenek az elsőrendű logika számára. A Davis–Putnam-algoritmus (Davis és Putnam, 1960) volt az első hatásos algoritmus az ítéletkalkulus rezolúció megvalósítására, de a legtöbb esetben ez is sokkal kevésbé hatékony, mint a DPLL visszalépéses algoritmus, amelyet két évvel később mutattak be (1962). A teljes rezolúciós szabály és a rezolúció teljességének bizonyítása J. A. Robinson (Robinson, 1965) nagyhatású tanulmányában jelent meg, ami azt is megmutatta, hogyan lehet elsőrendű logikai következtetést végezni ítéletkalkulus technikák igénybevétele nélkül.

Stephen Cook (Cook, 1971) mutatta meg, hogy a kielégíthetőség eldöntése az ítéletlogikában NP-teljes. Mivel a vonzat meghatározása ekvivalens a kielégíthetetlenség eldöntésével, ez is NP-teljes. Az ítéletlogika számos részhalmaza ismert, amelyről tudnuk, hogy bennük a kielégíthetőség problémája polinomiális időben megoldható. A Horn-klózok az egyik ilyen rézhalmaz. A Horn-klózokon működő, lineáris időben futó előreláncolási algoritmust Dowlingnak és Galliernek (Dowling és Gallier, 1984) köszönhetjük, akik az algoritmusokat egy adatfolyam-eljárásként írták le, hasonlóan a jelek terjedéséhez az áramkörökben. A kielégíthetőség ellenőrzése alapvető módszerré vált a problémák NP-teljességének vizsgálatában; például Kaye (Kaye, 2000), megmutatta, hogy az Aknakereső játék (lásd 7.11. feladat) NP-teljes.

Számos szerző próbálkozott lokális keresési algoritmusokat használni a kielégíthetőség eldöntésére a nyolcvanas években. Minden ilyen algoritmus a kielégíthetetlen klózok számának minimalizálásának elvén (Hansen és Jaumard, 1990) alapult. Különlegesen hatékony algoritmust fejlesztett ki Gu (Gu, 1989), és tőle függetlenül Selman és társai (Selman és társai, 1992), amelyet ez utóbbi szerzők GSAT-nak neveztek el, és megmutatták, hogy az algoritmus képes nehéz problémák széles körét igen gyorsan megoldani. A WALKSAT algoritmust, amelyet ebben a fejezetben bemutattunk, szintén Selma és társai publikálták (1996).

A „fázisátmenet” létezését a véletlen k-SAT problémák kielégíthetőségében először Simon és Dubois (Simon és Dubois, 1989) figyelték meg. Crawford és Auton tapasztalati eredményei (Crawford és Auton, 1993) azt sejtették, hogy nagyméretű, véletlenszerű 3-SAT problémák esetén ez az átmenet a 4,24-es klóz/változó arány környékén van. Cikkük szintén bemutat egy hatékony DPLL megvalósítást. Bayardo és Schrag leírt egy másik, kényszer-kielégítési technikákat alkalmazó hatékony DPLL megvalósítást (Bayardo és Schrag, 1997). Moskewicz és társai publikálták a CHAFF algoritmust (Moskewicz és társai, 2001), amely millió változós hardververifikációs problémákat képes megoldani, és amely megnyerte a SAT 2002 versenyt. Li és Anbulagan gyors problémamegoldókat lehetővé tevő egységpropagáción alapuló heurisztikákat tárgyalt (Li és Anbulagan, 1997). Cheeseman és társai (1991) számos hasonló problémáról adtak adatokat, és megfogalmazták azt a feltevést, hogy minden NP-teljes problémának van állapotátmenete (Cheeseman és társai, 1991). Kirkpatrick és Selman módszereket mutattak arra (Kirkpatrick és Selman, 1994), hogy a statisztikus fizika technikáit hogyan lehet alkalmazni a fázisátmenetek pontos „alakjának” jobb megértéséhez. Az átmenetek helyének meghatározására vonatkozó elméleti vizsgálatok igen gyengék: az egyetlen, amit sikerült bizonyítani, hogy az átmenet a [3,003 4,598] tartományba esik a véletlen 3-SAT problémáknál. Cook és Mitchell kiváló áttekintést készítettek ezekről és számos más kielégíthetőséggel kapcsolatos téma eredményeiről (Cook és Mitchell, 1997).

Korai elméleti kutatások megmutatták, hogy a DPLL átlagos komplexitása polinomiális a problémák egy bizonyos természetes eloszlású köreire. Ez a potenciálisan érdekes tény kevésbé izgalmassá vált, miután Franco és Paull megmutatták, hogy ugyanezek a problémák konstans időben megoldhatók egyszerűen találgatással, ahol véletlen hozzárendelésekkel dolgozunk (Franco és Paull, 1983). A véletlen generáló módszer, amelyet a fejezetben bemutattunk, sokkal nehezebb problémákat hoz létre. Az ilyen, a problémákon lokális kereséssel elért tapasztalati sikerek által motiválva, Koutsoupias és Papadimitriou megmutatta, hogy egy egyszerű hegymászó algoritmussal nagyon gyorsan megoldható szinte minden kielégíthetőségi probléma példány (Koutsoupias és Papadimitriou, 1992), ami azt sugallja, hogy a nehéz problémák ritkák. Mi több, Schöning bejelentett (Schönig, 1999) egy véletlen elemeket tartalmazó GSAT változatot, amelynek a legrosszabb esetre számított várható futási ideje 3-SAT problémákon 1,333n – ami még mindig exponenciális, de lényegesen gyorsabb, mint a korábbi legrosszabb esetkorlátok. A kielégíthetőségi algoritmusok ma is igen aktív területét képezik a kutatásoknak; Du és társai cikkgyűjteménye (Du és társai, 1999) jó kiindulási pontot jelent.

Az áramköralapú ágensek gondolata visszavezethető McCulloch és Pitts nagyhatású cikkére (McCulloch és Pitts, 1943), amely a neurális hálózatok témakör kezdetét jelentette. Népszerű vélekedésekkel szemben a cikk valójában logikai áramköralapú ágensterveknek az agyban történő megvalósításával foglalkozott. Azonban az áramköralapú ágens kis figyelmet kapott a mesterséges intelligenciában. A leginkább megjegyzendő kivétel Stan Rosenschein munkája (Rosenschein, 1985; Kaelbling és Rosenschein, 1990), aki módszert dolgozott ki áramköralapú ágensek lefordítására a feladat környezetének deklaratív leírására. A regiszterekben tárolt állítások frissítésének módszere közeli kapcsolatban van a Reiter által az elsőrendű logikára kifejlesztett követő állapot axiómához (successor-state axiom) (Reiter, 1991). Rod Brooks munkája (1986, 1989) demonstrálta az áramköralapú megvalósítások hatékonyságát robotok vezérlésére – a 25. fejezetben foglalkozunk ezzel a témával. Brooks amellett érvelt (Brooks, 1991), hogy az áramköralapú ágensen kívül más nem is szükséges a mesterséges intelligenciához – mivel más módszerek nehézkesek, drágák és szükségtelenek. A mi nézetünk szerint, egyik módszer sem elégséges önmagában.

A wumpus világot Gregory Yob (Yob, 1975) találta ki. Némi iróniával, Yob azért fejlesztette ki, mert unta azokat a játékokat, amelyeket egy rácson játszanak: az eredeti wumpus világ dodekaéder alakú volt, mi helyeztük vissza a régi unalmas négyzetrácsba. Michael Genesereth javasolta először, hogy a wumpus világot az ágensek tesztkörnyezeteként alkalmazzuk.

7.1.

Írja le a wumpus világot a 2. fejezetben felsorolt feladatkörnyezetek tulajdonságainak felhasználásával.

7.2.

Tegyük fel, hogy az ágens eljutott a 7.4. (a) ábra szerinti állapotba, úgy, hogy nem érzett semmit az [1, 1]-ben, szellőt érzett az [2, 1]-ben és bűzt az [1, 2]-ben, és most vizsgálja az [1, 3], [2, 2] és [3, 1] négyzetek tartalmát. Ezek bármelyike tartalmazhat csapdát, és legfeljebb az egyik tartalmazhatja a wumpust. A 7.5. ábra példáját követve hozza létre a lehetséges világokat (32 ilyet kell találnia). Jelölje meg azokat a világokat, amelyekben a TB igaz, és azokat, amelyekben a következő mondatok igazak:

α2 = „Nincsen csapda a [2, 2]-ben”

α 3 = „Az [1,3]-ban wumpus van”

Mutassa meg ezenkívül, hogy TB ⊨ α ₂ és TB ⊨ α ₃.

7.3.

Tekintsük azt a problémát, hogy hogyan dönthető el egy ítéletkalkulus mondat igazsága egy adott modellben.

7.4.

Bizonyítsa be a következő állításokat:

7.5.

Vegyünk egy szótárat, amelyben csak négy ítéletkalkulus állítás létezik, az A, B, C és D. Hány modellje létezik a következő mondatoknak?

7.6.

Definiáltunk 4 bináris logikai összekötőjelet.

7.7.

Egy szabadon választott módszer felhasználásával igazolja a 7.11. ábra ekvivalenciáit.

7.8.

Vizsgálja meg a következő mondatokat, és döntse el mindegyikre, hogy érvényesek, kielégíthetetlenek, vagy egyik sem. Igazolja a döntését igazságtáblával, vagy felhasználva a 7.11. ábra ekvivalencia szabályait. Van-e olyan, amit elsőre eltévesztett?

7.9.

(Barwise és Etchemendy, 1993 alapján) Be tudja-e bizonyítani, hogy az unikornis mitikus, ha adottak az alábbiak? Mit mondhatunk a mágikusságról? Van-e szarva?

Ha az unikornis mitikus, akkor halhatatlan, de ha nem halhatatlan, akkor egy halandó emlős. Ha az unikornis vagy halhatatlan, vagy emlős, akkor van szarva. Az unikornis mágikus állat, ha van szarva.

7.10.

Minden logikai mondat logikailag ekvivalens azzal az állítással, hogy minden lehetséges világ, amelyben hamis volna, nem az eset. Felhasználva ezt a megfigyelést, bizonyítsa be, hogy minden mondat átírható konjugált normált formára.

7.11.

Az ismert számítógépes játék, az Aknakereső igen hasonló a wumpus világhoz. Az aknakereső világ egy N négyzetet tartalmazó négyzetes rács, amelyek közül M elszórtan elhelyezkedő négyzet láthatatlan aknát takar. Minden négyzetet megpróbálhat az ágens, de azonnali halállal lakol, ha ott egy aknát talál. Az Aknakereső játék minden kipróbált négyzetben felfedi, hogy hány közvetlenül vagy átlósan szomszédos négyzetben van akna, ezzel mutatva az aknák jelenlétét. A cél az, hogy minden aknát nem tartalmazó négyzetet megpróbáljunk.

7.12.

Ez a feladat a klózok és az implikációs mondatok közötti kapcsolatot vizsgálja.

7.13.

Ebben a feladatban tervezze tovább az áramkörön alapuló wumpus ágenst.

7.14.

Elemezze, hogy mit is jelent az optimális viselkedés a wumpus világban! Mutassa meg, hogy az IT-WUMPUS-ÁGENS definíciója nem optimális, és tegyen javaslatot a fejlesztésére!

7.15.

7.16.

Mennyi ideig tart a DPLL számára a bizonyítása, ahol α egy literális, amelyet már tartalmaz a TB? Adjon magyarázatot!

7.17.

Kövesse a DPLL viselkedését a 7.15. ábrán leírt tudásbázison, amikor Q-t próbáljuk meg bizonyítani, és hasonlítsa össze ezt a működést az előrefelé láncolási algoritmussal.