A logikai következtetéseket széles körben vizsgálták már az ókori görög matematikusok is. Az Arisztotelész által legtöbbet vizsgált következtetési módszer a szillogizmus (syllogism) volt. A szillogizmus „szituációkra” és „hangulatokra” bontható a termek mondatbeli sorrendjétől függően (amelyeket predikátumoknak nevezünk ma) és az egyes termek általánosságának mértékétől függően (amit ma a kvantorok segítségével értelmezünk), illetve attól függően, hogy a termek negálva voltak-e. A legalapvetőbb szillogizmus, amely az első szituáció első hangulata, a következő:

Minden S az M is.

Minden M a P is.

Ezért minden S a P is.

Arisztotelész más szillogizmusok érvényességét is megpróbálta igazolni, visszavezetve ezeket az első szituációra. Pontosan leírta az egyes szillogizmusokhoz tartozó hangulatokat és szituációkat, de a szillogizmusok igazolása már kevésbé volt precíz.

Gottlob Frege, aki teljes elsőrendű logikát fejlesztett ki 1879-ben, következtetési rendszerét logikailag érvényes sémák nagyméretű gyűjteményére és egyetlen következtetési szabályra alapozta, a Modus Ponensre. Frege kihasználta azt a tényt, hogy ennek a formának „A P-ből következtesd a Q-t” következtetési szabályának a hatását szimulálhatja a Modus Ponens alkalmazásával a P-re, egy logikailag érvényes sémával, a P ⇒ Q-val. A kifejezésnek ezt az „axiomatikus” stílusát, amely a Modus Ponenst, plusz számos logikailag érvényes sémát használ, Frege után még számos matematikus használta; a leginkább említésre méltó, hogy a Principia Mathematicában (Whitehead és Russell, 1910) is felhasználták.

A következtetési szabályok, mint az axiomatikus sémáktól különálló dolgok álltak a természetes dedukció (natural deduction) központjában, amelyet Gerhard Gentzen és Stanislaw Jáskowski vezetett be (Gentzen, 1934; Jáskowski, 1934). A természetes dedukciót azért nevezik „természetesnek”, mert nem kívánja meg a mondatok átalakítását az (olvashatatlan) normál formára, és következtetési szabályaikat úgy tervezték, hogy az emberek számára természetesnek tűnjenek. Prawitz egy egész könyv hosszúságú elemzést adott a természetes dedukcióról (Prawitz, 1965). Gallier az automatikus dedukció elméleti alátámasztásának kifejtéséhez alkalmazta Gentzen szekvenciáit (Gallier, 1986).

A klózforma felfedezése nagy jelentőségű lépés volt az elsőrendű logika matematikai elemzésének kifejlesztésében. Whitehead és Russell (Whitehead és Russell, 1910) kiterjesztették az úgynevezett átviteli szabályt [maga a kifejezés Herbrandtól származik (Herbrand, 1930)], amit a kvantoroknak a formula elé történő kiemelésére alkalmaztak. A Skolem-konstansokat és a Skolem-függvényeket, viszonylag precíz leírást adva, Thoralf Skolem vezette be (Skolem, 1920). A skolemizáció teljes eljárása, a Herbrand-univerzum fontos fogalmának bevezetésével együtt egy későbbi írásban található (Skolem, 1928).

Herbrand elmélete, amit Jacques Herbrand francia matematikusról neveztek el, fontos szerepet játszott az automatikus következtető rendszerek módszereinek fejlesztésében, mind a Robinsonhoz fűződő rezolúció bevezetése előtt és után (Herbrand, 1930). Ezt tükrözi az, hogy habár maga a fogalom valójában Skolem eredménye, erre „Skolem-univerzum” helyett „Herbrand-univerzumként” hivatkozunk. Herbrandot említhetjük még az egyesítés felfedezőjeként is, mivel az egyesítés algoritmus egy változata megtalálható a (Herbrand, 1930)-ban. Gödel (Gödel, 1930) mutatta meg, Skolem és Herbrand elméleteire építve, hogy az elsőrendű logikának létezik teljes bizonyítási eljárása. Alan Turing és Alonzo Church egymástól függetlenül, igen különböző bizonyításokat alkalmazva megmutatták, hogy az érvényesség kérdése az elsőrendű logikában nem eldönthető (Turing, 1936; Church 1936). Enderton kiválóan megfogalmazott írása egy precíz, de viszonylag érthető stílusban magyarázza el ezeket az eredményeket (Enderton, 1972).

Habár McCarthy (McCarthy, 1958) javasolta először az elsőrendű logika használatát reprezentációs feladatokra és következetésre az MI-ben, az első ilyen rendszert a matematikai tételbizonyítás iránt érdeklődő matematikai logika kutatói fejlesztették ki. Abraham Robinson javasolta először, hogy használják az ítéletlogikára történő átalakítást és Herbrand-elméletet együtt. Gilmore (Gilmore, 1960) készített először egy olyan programot, amely ezen a megközelítésen alapult. Davis és Putnam (Davis és Putnam, 1960) vezették be a klózformát, és hoztak létre egy olyan programot, amely megkísérelt cáfolatokat találni, oly módon, hogy a Herbrand-univerzum elemeit a változók helyére alapklózokat helyettesítve és ítéletinkonzisztenciákat keresve az alapklózok között. Prawitz (Prawitz, 1960) vezette be azt az alapötletet, hogy az ítéletinkonzisztencia lekérdezése vezesse a keresési folyamatot, és azt is, hogy csak akkor hozzunk létre termeket a Herbrand-univerzumban, hogyha ez szükséges az ítélet-inkonzisztencia megállapítása céljából. Más kutatók egyéb fejlesztései után, ez a gondolat vezette el J. A. Robinsont (nem rokona az előzőnek) a rezolúció módszerének kifejlesztéséhez (Robinson, 1965). Az úgynevezett „inverz módszer”, amit egyidejűleg fejlesztett ki S. Maslov szovjet kutató, kissé eltérő elveken alapult, mint Robinson rezolúciós módszere, de hasonló számítási előnyöket nyújt a propozicionalizációhoz képest (Maslov, 1964, 1967). Wolfgang Bibel kapcsolati módszere (connection method) e megközelítés kiterjesztésének tekinthető.

A rezolúció kifejlesztése után az elsőrendű következtetéssel foglalkozó munkák különböző irányokban ágaztak el. Az MI-ben a rezolúciót a kérdés-válasz rendszerekre adoptálta Cordell Green és Bertram Raphael (Green és Raphael, 1968). Egy kevésbé formális megközelítést alkalmazott Carl Hewitt (Hewitt, 1969). Az ő PLANNER nyelve, habár sohasem valósították meg teljességében, előfutára volt a logikai programozásnak, és útmutatásokat tartalmazott az előrefelé és hátrafelé láncoláshoz, valamint a negáltak sikertelenségének vizsgálati módszeréhez. Az eredeti nyelv egy részét, a MICRO-PLANNER-t (Sussman és Winograd, 1970) megvalósították és felhasználták az SHRDLU természetes nyelvek megértését segítő rendszerben (Winograd, 1972). A korai MI-alkalmazások jelentős erőfeszítést tettek olyan adatstruktúrák előállítására, amelyek lehetővé teszik tények hatékony előhívását. Ezeket a munkákat is bemutatják az MI-programozással kapcsolatos cikkek (Charniak és társai, 1987; Norvig, 1992; Forbus és de Kleer, 1993).

A hetvenes évek elejére az előrefelé láncolás (forward chaining) jól megalapozottnak tekinthető az MI-ben, egy könnyen érthető alternatívája lett a rezolúciónak. Rendszerek széles körében került felhasználásra, Nevins geometriai tételbizonyítójától (Nevins, 1975) a VAX konfigurációjához használt R1 szakértői rendszerig (McDermott, 1982). Az MI-alkalmazások jellemzően nagyszámú szabályt tartalmaztak, tehát fontos volt kifejleszteni hatékony szabályillesztési technológiát, különösen az inkrementális frissítések problémájára. A produkciós rendszerek (production systems) technológiáját azért fejlesztették ki, hogy segítse az ilyen típusú az alkalmazások megvalósítását. Az OPS-5 produkciós rendszer nyelvet (Forgy, 1981; Brownston és társai, 1985) használták az R1-hez és a SOAR kognitív szerkezetéhez (Laird és társai, 1987). Az OPS-5 tartalmazta a rete illesztési folyamatot is (Forgy, 1982). A SOAR, amely új szabályokat generál, hogy megőrizze a megelőző számítások eredményeit, igen nagy szabályhalmazokat állíthat elő – több mint 1 000 000 szabályt a TACAIR-SOAR rendszer esetében, amely katonai repülőgépek szimulációját kontrollálja (Jones és társai, 1998). A CLIPS (Wygant, 1989) egy C-alapú produkciós rendszer nyelv, amelyet a NASA-nál fejlesztettek ki, és hatékony integrációt tett lehetővé más programokkal, eszközökkel és érzékelő rendszerekkel, valamint felhasználták űrjárművek automatizálására és egyéb harcászati alkalmazásokra.

A deduktív adatbázisokként (deductive databases) ismert kutatási terület szintén hozzájárult az előrefelé következtetés megértéséhez. Egy Toulouse-i szellemi műhelyben kezdődött a munka 1977-ben, amelyet Jack Minker szervezett, összehozva a logikai következtetési és az adatbázisrendszerekkel foglalkozó szakembereket (Gallaire és Minker, 1978). Egy történeti áttekintés (Ramakrishnan és Ullman, 1995) szerint: a „deduktív [adatbázis-] rendszerek megkísérlik a Prolog adaptálását, a »kis mennyiségű adat« megközelítésről a »nagymennyiségű adat« világára.” Így tehát, ennek a munkának a célja az, hogy egybeolvassza a relációs adatbázis technológiát, amelyet nagyméretű tényhalmazok előhívására terveztek, a Prolog-alapú következtetési technológiával, amely jellemzően egyszerre csak egy tényt hív elő. A deduktív adatbázisokról szóló szövegek közé tartoznak az (Ullman, 1989) és a (Ceri és társai, 1990) munkák.

Chandra és Harel (Chandra és Harel, 1980), valamint Ullman (Ullman, 1985) nagy hatású munkái a Datalognak mint egy, a deduktív adatbázisokhoz kidolgozott standard nyelvnek az elfogadásához vezettek. Az „alulról felfelé” irányú következtetés, az előrefelé láncolás szintén standard lett – részben azért, mert elkerüli a leállási problémákat és a felesleges számítások problémáját, amely a hátrafelé láncolásnál előfordul, és részben azért, mert természetesebben felhasználható az alapvető relációs adatbázis-operációkhoz. A mágikus halmazok (magic sets) technikája a szabályok átírására, amelyet Bancilhon (Bancilhon és társai, 1986) fejlesztettek ki, lehetővé tette az előrefelé láncolásnak, hogy a hátrafelé láncolástól kölcsönözze a célorientáltság előnyös tulajdonságát. A „fegyverkezési verseny” kiegyenlítése céljából, a táblázatos logikai programozási módszerek kölcsönveszik a dinamikus programozás előnyét az előrefelé láncolástól.

A logikai következtetések komplexitásáról szerzett tudásunk legnagyobb része a deduktív adatbázisokkal foglalkozó tudományos közösségből származik. Chandra és Merlin (Chandra és Merlin, 1977) mutatták ki először, hogy egy egyszerű nem rekurzív szabály (vagyis egy konjunktív lekérdezés (conjunctive query) az adatbázisok terminológiájában) illesztése NP-nehéz lehet. Kuper és Vardi (Kuper és Vardi, 1993) javasolták az adatkomplexitás (data complexity) használatát – annak a mértéknek a használatát, ami a komplexitást, mint az adatbázis méretének egy függvényét méri, miközben a szabály méretét konstansnak tekinti – a lekérdezések megválaszolásának mértékére. Gottlob és társai (Gottlob és társai, 1999b) a konjuktív lekérdezések és a kényszerkielégítés közötti kapcsolatot vizsgálták, megmutatva, hogy a hiper-fák lebontása hogyan optimizálja az illesztési folyamatot.

Mint azt már előzőleg említettük, a hátrafelé láncolás (backward chaining) Hewitt PLANNER nyelvében jelent meg a logikai következtetéshez (Hewitt, 1969). A logikai következtetés magától értetődően ettől a munkától függetlenül fejlődött tovább. A lineáris rezolúció egy korlátozott változatát, amelyet SL-rezolúciónak (SL-resolution) nevezünk, Kowalski és Kuehner (Kowalski és Kuehner, 1971) fejlesztette ki Loveland modelleliminációs (model elimination) technikájára építve (Loveland, 1968). Ennek a határozott klózokra alkalmazott változata az SLD-rezolúció (SLD-resolution), amely önmagában alkalmas határozott klózok, mint programok interpretálására (Kowalski, 1974; 1979a; 1979b). Ezalatt, 1972-ben, a francia kutató, Alain Colmerauer kifejlesztette és alkalmazni kezdte a Prologot, a természetes nyelvek elemzésének céljából. A Prolog klózait először kontextusmentes nyelvtani szabályoknak szánták (Roussel, 1975; Colmerauer és társai, 1973). Az elméleti háttér túlnyomó részét a logikai programozás részére Colmerauerrel együttműködve Kowalski fejlesztette ki. A szemantikai definíció, amely a rögzített pontokat használja, Van Emdennek és Kowalskinak köszönhető (Van Emden és Kowalski, 1976). Kowalski (Kowalski, 1988) és Cohen (Cohen, 1988) jó történeti áttekintést nyújtanak a Prolog eredetéről. A Logikai programozás alapjai (Foundations of Logic Programming) (Lloyd, 1987) egy elméleti elemzése a Prolog és egyéb logikai programozónyelvek megalapozásának.

A hatékony Prolog fordítókat általában a Warren Abstract Machine (WAM) számítási modelljére alapozzák, amelyet David H. D. Warren (Warren, 1983) fejlesztett ki. Van Roy (Van Roy, 1990) megmutatta, hogy a további fordítási technikák alkalmazása, mint amilyen a típusinterferencia, versenyképessé teszi a Prolog programokat a C programokkal a sebesség tekintetében. A Japán Ötödik Generációs projekt, amely egy 1982-ben kezdődő 10 éves kutatási erőfeszítés volt, teljes egészében a Prologon, mint az intelligens rendszerek kifejlesztésének alapeszközén alapult.

A rekurzív logikai programok felesleges ciklusainak elkerüléséhez egymástól függetlenül Smith (Smith és társai, 1986), valamint Tamaki és Sato (Tamaki és Sato, 1986) fejlesztettek ki módszereket. Az utóbbi tanulmány tartalmazta a memók gyűjtését is a logikai programokra, egy olyan módszert, amelyet teljes mértékben David S. Warren fejlesztett ki a táblázatos logikai programozás (tabled logic programming) módszerében. Swift és Warren (Swift és Warren, 1994) bemutatták, hogy hogyan terjesszük ki a WAM-ot táblázatok kezelésére, amely képessé tette a Datalog programokat, hogy egy nagyságrenddel gyorsabban fussanak, mint az előrefelé láncolást alkalmazó deduktív adatbázisrendszerek.

A korai elméleti munkákat a korlátozott logikai programozás területén Jaffar és Lassez végezték (Jaffar és Lassez, 1987). Jaffar és társai (Jaffar és társai, 1992a) kifejlesztették a CLP(R) rendszert a valós értékű kényszerek kezelésére. Jaffar (Jaffar és társai, 1992b) általánosította a WAM-ot, létrehozva ezzel a CLAM-ot (Korlátozott Logikai Absztrakt Gép, Constraint Logic Abstract Machine) a CLP megvalósításainak specifikálásához. Ait-Kaci és Podelski (Ait-Kaci és Podelski, 1993) bemutattak egy kifinomult LIFE-nak nevezett nyelvet, amely egyesíti a CLP-t a funkcionális programozással és az öröklődés következtetéssel. Kohn (Kohn, 1991) egy ambiciózus projektet mutat be a korlátozott logikai programozás használva, a valós idejű vezérlési architektúrákat megalapozva, teljesen automata pilóták alkalmazására.

A logikai programozásról és a Prologról számos könyvet írtak. A Logika a problémamegoldáshoz (Logic for Problem Solving) (Kowalski, 1979b) egy korai általános tanulmány a logikai programozásról. A Prologgal foglalkozó könyvek közé tartoznak Clocksin és Mellish (Clocksin és Mellish, 1994), Shoham (Shoham, 1994) és Bratko (Bratko, 2001) írásai. Marriott és Stuckey (Marriott és Stuckey, 1998) kitűnő leírását adják a CLP-nek. A 2000-ben történt megszűnéséig a Journal of Logic Programming volt a téma legfontosabb folyóirata; helyét mára átvette a Theory and Practice of Logic Programming. A logikai programozások konferenciái között a legjelentősebbek az International Conference on Logic Programming (ICLP) és az International Logic Programming Symposium (ILPS).

A kutatások a matematikai tételbizonyítások (mathematical theorem proving) területén már az első teljes elsőrendű logikai rendszerek kifejlesztése előtt megkezdődtek. Herbert Gelernter Geometriai Tételbizonyítója (Gelernter, 1959) heurisztikai keresési módszereket használt diagramokkal kombinálva, hogy kiselejtezze a hamis részcélokat, és képes volt bebizonyítani néhány nagyon bonyolult eredményt az euklideszi geometriában. Ettől kezdve azonban nem volt jelentős együttműködés a tételbizonyítás és az MI között.

A korai munkák a teljességre koncentráltak. Robinson korszakalkotó tanulmányát követően a demodulációs és a paramodulációs szabályokat az egyenlőségi következtetésekre Wos (Wos és társai, 1967), valamint Wos és Robinson (Wos és Robinson, 1968) vezették be, ebben a sorrendben. Ezeket a szabályokat a term átírási rendszerek kontextusában is kifejlesztették (Knuth és Bendix, 1970). Az egyenlőségi következtetés beépítése az egyesítési algoritmusba Gordon Plotkinnak köszönhető (Plotkin, 1972); ez fontos vonása volt a QLISP-nek is (Sacerdoti és társai, 1976). Jouannaud és Kirchner (Jouannaud és Kirchner, 1991) az egyenlőségi egyesítést a termek átírásának szempontjából vizsgálják. Hatékony algoritmusokat a standard egyesítésre Martelli és Montanari (Martelli és Montanari, 1976), valamint Paterson és Wegman (Paterson és Wegman, 1978) fejlesztettek ki.

Az egyenlőségi következtetések mellett a tételbizonyítások tartalmaztak különféle speciális célú döntési folyamatokat. Nelson és Oppen (Nelson és Oppen, 1979) javasoltak egy nagy hatású sémát az ilyen eljárásoknak egy általános következtetési rendszerbe integrálására. Más módszerek is hasonló problémákkal foglalkoztak, beleértve Stickel (Stickel, 1985) „elméleti rezolúcióját”, valamint Manna és Waldinger (Manna és Waldinger, 1986) „speciális relációit”.

Számos vezérlési stratégiát javasoltak a rezolúcióra, kezdve az egységpreferencia stratégiával (Wos és társai, 1964). A támogató halmaz stratégiát Wos (Wos és társai, 1964) javasolta, hogy biztosítson egy bizonyos fokú célorientáltságot a rezolúcióban. A lineáris rezolúció először Lovelandnél (Loveland, 1970) jelent meg. Genesereth és Nilsson (Genesereth és Nilsson, 1987, 5. fejezet) rövid, de átfogó elemzést nyújtanak a vezérlési stratégiák széles skálájáról.

Guard és társai (Guard és társai, 1969) egy korai SAM tételbizonyítót írnak le, amely segített megoldani egy megoldatlan problémát a rácselméletben. Wos és Winkler (Wos és Winkler, 1983) áttekintést nyújtanak az AURA tételbizonyító eredményeiről, amelyeket a matematika és a logika különböző területein fellelhető problémák megoldása terén ért el. McCune (McCune, 1992) ezt folytatja, amikor felhasználja ezeket az eredményeket az AURA utódjának, az OTTER-nek alkalmazásában megoldatlan problémák megoldására. Weidenbach (Weidenbach, 2001) bemutatja a SPASS-t, az egyik legerőteljesebb jelenlegi tételbizonyítót. A Computational Logic (Boyer és Moore, 1979) című könyv az alapreferencia a Boyer–Moore-tételbizonyítókhoz. Stickel (Stickel, 1988) leírja a Prolog Technológiai Tételbizonyítót (PTTP), amely egyesíti a Prolog fordítás előnyeit a modell elimináció teljességével (Loveland, 1968). A SETHEO (Letz és társai, 1992) egy másik széles körben használt tételbizonyító, amely hasonló megközelítésen alapul; másodpercenként több millió következtetést tud végrehajtani egy 2000-es munkaállomáson. A LEANTAP (Beckert és Posegga, 1995) hatékony tételbizonyító, amelyet mindössze 25 Prolog sorral valósítottak meg.

Az automata programszintézisről szóló korai munkákat Simon (Simon, 1963), Green (Green, 1969a), valamint Manna és Waldinger (Manna és Waldinger, 1971) készítették. Burstall és Darlington transzformációs rendszere (Burstall és Darlington, 1977) egyenlőség következtetést használt a rekurzív programszintézishez. A KIDS (Smith, 1990, 1996) az egyik legerősebb modern rendszer; amely egy szakértő segédeszközként működik. Manna és Waldinger (Manna és Waldinger, 1992) egy áttekintő bevezetést adtak a témakör aktuális helyzetéről fókuszba állítva a saját deduktív megközelítésüket. Az Automating Software Design (Lowry és McCartney, 1991) számos, a témáról szóló tanulmányt gyűjtött össze. A logikának a hardvertervezésben való felhasználásáról Kern és Greenstreet (Kern és Greenstreet, 1999) adott egy áttekintést; Clarke (Clarke és társai, 1999) műve pedig a modellellenőrzéssel foglalkozik a hardververifikálásban.

A Computability and Logic (Boolos és Jeffrey, 1989) egy jó referencia a teljesség és a nem eldönthetőség témaköréhez. Számos korai tanulmány a matematikai logikáról megtalálható a From Frege to Gödel: A Source Book in Mathematical Logic (van Heijenoort, 1967) című könyvben. A tiszta matematikai logika témakörének folyóirata a Journal of Symbolic Logic. Az automatizált dedukció irányába haladó könyvek közé tartozik a klasszikus Symbolic Logic and Mechanical Theorem Proving (Chang és Lee, 1973), és számos más írás, köztük Wos, Bibel és Kaufmann később íródott munkái (Wos és társai, 1992; Bibel, 1993; Kaufmann és társai, 2000). Az Automation of Reasoning c. antológia (Siekmann és Wrightson, 1983) sok fontos korai tanulmányt tartalmaz az automatizált dedukcióról. További áttekintő műveket írtak Loveland (Loveland, 1984) és Bundy (Bundy, 1999). A legjelentősebb folyóirat a tételbizonyítások területén a Journal of Automated Reasoning; a legfontosabb konferencia az évente megtartott Conference on Automated Deduction (CADE). A tételbizonyítás területén folyó kutatás szintén szoros kapcsolatban áll a logika használatával a programok és programozási nyelvek elemzésében, amely tárgyban a legfőbb konferencia a Logic in Computer Science.

9.1.

Vezesse le az alaptételekből, hogy az univerzális példányosítás helyes, és azt, hogy az egzisztenciális példányosítás következtetési szempontból egyenértékű tudásbázist hoz létre.

9.2.

A Szereti( János, Fagylalt) mondatból kiindulva logikusnak tűnik arra következtetni, hogy ∃x Szereti(x, Fagylalt). Adjon meg egy általános következtetési szabályt, az egzisztenciális bevezetést (Existential Introduction), amely megerősíti ezt a következtetést. Gondosan vizsgálja meg a feltételeket, amelyeket ki kell elégíteni a felhasznált változókkal és termekkel.

9.3.

Tételezzük fel, hogy egy tudásbázis csak egy mondatot tartalmaz: ∃x OlyanMagasMint(x, Everest). A következők közül melyek a törvényszerű következményei az Egzisztenciális Példányosítás alkalmazásának?

(a szabály kétszeri alkalmazása után).

9.4.

Adja meg az alábbi atomi mondatpárok legáltalánosabb egyesítőjét, ha egyáltalán létezik ilyen:

9.5.

Figyelje meg a 9.2. ábrán bemutatott bennfoglalási rácsokat.

9.6.

Tételezzük fel, hogy betöltjük egy logikai adatbázisba az amerikai választási címjegyzéket, amely felsorolja a korát, a lakóhelyét, a születési dátumát és az anyja nevét minden személynek, társadalombiztosítási számokat használva azonosító adatként. Így tehát György kora így van megadva: Kora(443-65-1282, 56). A következő S1–S5 indexelő sémák melyike tesz lehetővé hatékony megoldást a Q1–Q4 lekérdezésekre (tekintsünk egy normál hátrafelé láncolást)?

9.7.

Feltételezhetnénk, hogy az egyesítés során a változó konfliktus problémáját elkerülhetjük úgy, ha minden mondatnál egyszerre átnevezzük az összes változót a tudásbázisban. Mutassa meg, hogy léteznek olyan mondatok, amelyekre ez a megközelítés nem alkalmazható. (Segítség: tekintsünk egy olyan mondatot, amelynek egyik része egyesíthető a többivel.)

9.8.

Mutassa meg, hogy hogyan írhatunk meg egy tetszőleges méretű adott 3-SAT problémát, egy elsőrendű határozott klózt és nem több, mint 30 alaptényt felhasználva.

9.9.

Adja meg az alábbi mondatok olyan logikai reprezentációját, amely alkalmas arra, hogy az Általánosított Modus Ponens szabályt alkalmazzuk rájuk:

9.10.

Ebben a problémában a 9.4. feladatban bemutatott mondatokat fogjuk használni. Válaszolja meg a következő kérdéseket hátrafelé láncolást alkalmazva!

9.11.

Egy népszerű találós kérdés gyerekeknek a következő: „Nincs se bátyám, se nővérem, mégis annak az embernek az apja az én apám fia.” Használja fel a család tárgykör szabályait (lásd 7. fejezet), és mutassa meg, hogy ki is az említett ember. Használhatja bármelyik, a fejezetben bemutatott következtetési módszert.

9.12.

Kövesse nyomon a 9.6. ábrán látható hátrafelé láncolási algoritmus végrehajtását, amikor azt a bűntény probléma megoldására alkalmazzuk. Mutassa be azt az érték-szekvenciát, amelyet a célok változó vesz fel, és rendezze egy fa formába.

9.13.

A következő Prolog kód egy P predikátumot határoz meg:

P(X,[XС∣Y])

P(X,[Y∣Z]):-P(X,Z)

9.14.

9.15.

9.16.

Ebben a feladatban megvizsgáljuk a keresési algoritmusok alkalmazását a Prologban. Tételezzük fel, hogy a következő(X, Y) akkor igaz, ha az Y állapot az X állapotot követi; és ha a cél(X) akkor igaz, amikor az X a célállapot. Írjon egy definíciót a megold(X,P)-re, ami azt jelenti, hogy a P az útvonal (az állapotok listája), amely az X-szel kezdődik, a célállapotban végződik, és szabályos lépésekből áll, amelyeket a következő határoz meg. Valószínűleg a mélységi keresés a legkönnyebb módja annak, hogy ezt végrehajtsa. Mennyire lenne könnyű egy heurisztikus keresési vezérlés hozzáadása?

9.17.

Hogyan alkalmazható a rezolúció annak megmutatásra, hogy egy mondat

9.18.

Abból a mondatból, hogy „a lovak állatok” következik-e, hogy „egy ló feje egy állat feje”. Demonstrálja, hogy ez a következtetés érvényes, ha végrehajtjuk a következő lépéseket:

9.19.

Tekintsük a következő két elsőrendű logikai mondatot:

(A): ∀x ∃y (x ≥ y)

(B): ∃y ∀x (x ≥ y)

9.20.

A rezolúció változókkal való lekérdezésekre létrehozhat nem konstruktív bizonyításokat, ezért egy speciális eljárást kell bevezetnünk a definit válaszok kinyerésére. Magyarázza meg, hogy ez a probléma miért nem merül fel csak definit klózokat tartalmazó tudásbázisokkal!

9.21.

Ebben a fejezetben azt mondtuk, hogy a rezolúció nem használható egy mondathalmaz összes logikai következményének a generálására. Van olyan algoritmus, ami képes erre?