Logische agenten en planning

Een kennisgebaseerde agent handelt op basis van een beschrijving van zijn wereld. Zijn kennisbank (KB) bevat formele uitspraken: aanvankelijke feiten en regels, axioma's genoemd, en informatie die tijdens de werking wordt toegevoegd. Inferentie verbindt die uitspraken met conclusies die de agent nooit rechtstreeks heeft waargenomen.

Verbind waarneming met actie

TELL voegt een uitspraak toe aan de KB. ASK vraagt om een antwoord dat door de KB wordt ondersteund, al opgeslagen of afgeleid. Bij elke tijdstap legt de agent zijn waarneming vast, vraagt hij welke actie hij moet kiezen, legt hij de gekozen actie vast en voert hij die uit. Acties vastleggen is belangrijk omdat latere redeneringen moeten weten hoe de wereld is veranderd.

Op het kennisniveau kunnen we zeggen dat een robot weet dat een doorgang geblokkeerd is en een opslagruimte wil bereiken. Op het implementatieniveau beschrijven we datastructuren en inferentieprocedures. Een declaratief ontwerp levert feiten en regels; een procedureel ontwerp schrijft gedrag rechtstreeks in code. Een werkende agent kan beide combineren.

Lees de wumpuswereld

De wumpuswereld is een rooster van 4 × 4. Coördinaten zijn [kolom, rij]; de agent begint in [1, 1] en kijkt naar rechts. Er is één wumpus, één stuk goud en in elk vak behalve het startvak is de kans op een put 0,2. Putten en de wumpus blijven op hun plaats. De wereld is discreet, deterministisch en bevat één agent, maar is gedeeltelijk waarneembaar: de indeling is verborgen.

Een Bries geeft aan dat er een put in een direct aangrenzend vak is; Stank geeft aan dat de wumpus daar zit. Diagonale vakken tellen niet mee. Schittering duidt op goud in het huidige vak, Botsing meldt een muur en Kreet meldt de dood van de wumpus, waar die ook in de grot plaatsvindt. De acties zijn Vooruit, DraaiLinks, DraaiRechts, Pak, Schiet en Klim. De agent heeft één pijl; Klim verlaat de grot alleen vanuit [1, 1]. Vertrekken met goud levert 1000 punten op, sterven kost 1000 punten, elke actie kost 1 punt en schieten kost nog eens 10 punten.

Combineer waarnemingen

In [1, 1] sluit de afwezigheid van een Bries putten in [1, 2] en [2, 1] uit; de afwezigheid van Stank sluit de wumpus daar uit. Beide vakken zijn veilig. In [2, 1] geeft een Bries aan dat er een put in [2, 2] of [3, 1] zit, omdat het startvak er geen heeft. De afwezigheid van Stank sluit de wumpus in [2, 2] en [3, 1] uit.

De agent bezoekt daarna [1, 2]. De afwezigheid van een Bries sluit een put in [2, 2] uit, dus dwingt de eerdere disjunctie een put in [3, 1] af. Stank in [1, 2] plaatst de wumpus in [1, 3] of [2, 2]. De eerdere waarneming zonder Stank sluit [2, 2] uit, zodat [1, 3] overblijft. De agent heeft vastgesteld dat [2, 2] geen van beide gevaren bevat zonder het vak te betreden.

Deze redenering hangt af van zowel de waarnemingen als de regels die waarnemingen aan gevaren verbinden. Een onverkend vak is onbekend wanneer de KB noch veiligheid, noch gevaar ondersteunt. Gevaar niet kunnen afleiden is onvoldoende om te stellen dat het veilig is. Kiezen om zo'n vak te betreden vereist een beslissing over risico, die verder gaat dan alleen de logische gevolgen.

Propositielogica geeft een agent precieze regels om beweringen met een ja-of-neeantwoord te combineren. Een atomair symbool benoemt een volledige bewering, zoals P₁₂ voor “er is een put in [1, 2]”. Een literaal is een atomaire uitspraak of de negatie daarvan. Grotere uitspraken combineren die met ¬, ∧, ∨, ⇒ en ⇔.

Beoordeel de connectieven

Een model kent aan elk symbool waar of onwaar toe. Met n symbolen zijn er 2ⁿ waardetoekenningen. Negatie keert een waarheidswaarde om; bij een conjunctie moeten beide kanten waar zijn; bij een inclusieve disjunctie minstens één. Een implicatie is alleen onwaar als de voorwaarde waar en de conclusie onwaar is. Bij een bi-implicatie moeten de waarheidswaarden aan beide kanten gelijk zijn.

De bindingsvolgorde is ¬, ∧, ∨, ⇒, ⇔. Dus ¬A ∧ B ⇒ C betekent ((¬A) ∧ B) ⇒ C. Gebruik haakjes als de bedoelde groepering onduidelijk kan zijn. Als A waar, B onwaar en C waar is, dan is (A ∨ B) ⇒ C waar, terwijl A ⇒ (B ∧ C) onwaar is.

Een logische implicatie stelt een beperking aan waarheidswaarden, geen oorzaak. Een onware voorwaarde maakt de implicatie waar. Je mag ook de richting niet omkeren: uit “als de batterij leeg is, stopt de robot” kun je niet alleen op grond van het stoppen vaststellen dat de batterij leeg is.

Codeer beide richtingen van een regel

De briesregel voor het startvak is B₁₁ ⇔ (P₁₂ ∨ P₂₁). Die zegt dat er precies dan een bries is als er een put in een aangrenzend vak zit. De richting B₁₁ ⇒ (P₁₂ ∨ P₂₁) maakt het mogelijk om uit een bries gevaar af te leiden. De omgekeerde richting maakt het mogelijk om uit de afwezigheid van een bries een put uit te sluiten. Als je die weglaat, verlies je de afleiding van ¬P₁₂ ∧ ¬P₂₁ uit ¬B₁₁.

Elk vak heeft zijn eigen propositionele regel nodig. Om precies één wumpus onder 16 vakken te coderen, heb je een disjunctie voor minstens één nodig en een constraint voor hoogstens één per paar. Er zijn 16 × 15 / 2 = 120 verschillende paren. Propositionele symbolen kunnen niet over vakken kwantificeren, dus worden algemene regels veel afzonderlijke uitspraken.

Geef verandering weer zonder behoud te verliezen

Een veranderlijke toestandsuitspraak is een feit waarvan de waarheidswaarde kan veranderen. Een tijdstip in superscript onderscheidt de waarden: L₁₁⁰ legt de locatie op tijdstip 0 vast. Een effectaxioma kan zeggen dat naar rechts bewegen vanuit [1, 1] op tijdstip 1 de locatie [2, 1] oplevert en de oude locatie verwijdert. Het laat open wat er gebeurt met niet-gerelateerde feiten, zoals het bezit van de pijl. Al deze onveranderde feiten beschrijven is het frameprobleem.

Een opvolgertoestandsaxioma geeft één volledige actualisatieregel per veranderlijke toestandsuitspraak: Fᵗ⁺¹ ⇔ (een actie maakt F waar) ∨ (Fᵗ ∧ geen actie maakt F onwaar). Voor de pijl: HeeftPijlᵗ⁺¹ ⇔ (HeeftPijlᵗ ∧ ¬Schietᵗ). Zonder een actie die een andere pijl levert, blijft de agent de pijl houden totdat hij schiet en heeft hij daarna geen pijl meer.

Een agent heeft een criterium nodig om te bepalen of een conclusie gerechtvaardigd is. Logisch gevolg, geschreven als KB ⊨ α, betekent dat α waar is in elk model dat aan de KB voldoet. Eén passende wereld waarin α onwaar is, weerlegt het logische gevolg.

Houd precies de passende modellen over

Modelcontrole somt waardetoekenningen op, verwerpt die welke een uitspraak in de KB onwaar maken en toetst de zoekvraag in de overgebleven modellen. Stel dat de KB A ∨ B en ¬A bevat. Van de vier waardetoekenningen aan A en B voldoet alleen A onwaar, B waar aan beide uitspraken. Uit de KB volgen B en ¬A. A volgt er niet uit, omdat het overgebleven model A onwaar maakt.

In de wumpus-KB gebruiken ¬P₁₁, B₁₁ ⇔ (P₁₂ ∨ P₂₁), B₂₁ ⇔ (P₁₁ ∨ P₂₂ ∨ P₃₁), ¬B₁₁ en B₂₁ zeven symbolen. Er zijn 128 waardetoekenningen. Precies drie voldoen aan de KB: P₁₂ en P₂₁ zijn onwaar, terwijl P₂₂ en P₃₁ respectievelijk waar/onwaar, onwaar/waar of waar/waar zijn. Dus volgt ¬P₁₂ logisch. P₂₂ verschilt tussen de drie modellen, dus volgt noch P₂₂, noch ¬P₂₂ logisch. Deze putregels alleen stellen vast dat er geen put is, niet dat de wumpus afwezig is.

Onderscheid de belangrijkste logische toetsen

P ∨ ¬P is algemeengeldig; P ∧ ¬P is onvervulbaar. P ⇒ Q en ¬P ∨ Q zijn equivalent. Equivalentie vereist logisch gevolg in beide richtingen. Uit A ∧ B volgt A, maar A laat modellen toe waarin B onwaar is, dus geldt de omgekeerde gevolgtrekking niet.

Maak van een zoekvraag een tegenspraaktoets

KB ⊨ α precies wanneer KB ∧ ¬α onvervulbaar is. Door de ontkende zoekvraag toe te voegen, zoek je een wereld waarin de KB geldt en de zoekvraag niet. Als je die niet vindt, bewijst dat het logische gevolg; als je die wel vindt, geeft dat een tegenmodel. Gelijkwaardig daaraan geldt α ⊨ β precies wanneer α ⇒ β algemeengeldig is. Je kunt de algemeengeldigheid van α zelf toetsen door te controleren of ¬α onvervulbaar is.

Het connectief ⇒ hoort binnen een uitspraak. Het symbool ⊨ beschrijft een relatie tussen uitspraken en hun modellen. Zo kan “volgt niet logisch” betekenen dat de zoekvraag is uitgesloten of dat die onbekend blijft. Controleer of de negatie logisch volgt voordat je tussen beide kiest.

Enumeratie is correct en volledig voor propositielogica omdat ze een eindige verzameling uitputtend controleert. Diepte-eerst enumereren kost O(2ⁿ) tijd en O(n) geheugen; 50 symbolen leveren al ongeveer 1,13 × 10¹⁵ waardetoekenningen op. Bepalen of een propositionele uitspraak logisch volgt, is co-NP-volledig. Controleer ook de consistentie: uit een KB zonder modellen volgt elke uitspraak, omdat er geen passend model is dat een zoekvraag zou kunnen schenden.

Een bewijs leidt een zoekvraag af door regels toe te passen op al bekende uitspraken. KB ⊢ α legt een afleiding vast; KB ⊨ α legt een semantische garantie over modellen vast. Een correcte bewijsprocedure verbindt de twee: elke conclusie die ze afleidt, volgt werkelijk logisch. Een volledige procedure kan binnen de bedoelde taal elke conclusie afleiden die logisch volgt.

Pas regels toe op hun premissen

Modus ponens leidt uit P ⇒ Q en P de uitspraak Q af. En-eliminatie leidt uit P ∧ Q een van beide conjuncten af. Als SensorAan ∧ Gekalibreerd en SensorAan ⇒ MetingBeschikbaar bekend zijn, levert en-eliminatie SensorAan op en vervolgens modus ponens MetingBeschikbaar. Elke regel van het bewijs vermeldt de informatie en de regel die haar rechtvaardigen.

Deze regels behouden de waarheid, maar door hun beperkte vocabulaire zijn ze onvolledig als volledig bewijssysteem. Uit P volgt semantisch de uitspraak P ∨ Q, maar geen van beide regels introduceert ∨. Een verzameling correcte regels kan toch geldige conclusies missen.

Herschrijf zonder de betekenis te veranderen

Nuttige equivalenties kun je in beide richtingen toepassen:

• Dubbele negatie: ¬¬P ≡ P.
• Implicatie: P ⇒ Q ≡ ¬P ∨ Q.
• Contrapositie: P ⇒ Q ≡ ¬Q ⇒ ¬P.
• Bi-implicatie: P ⇔ Q ≡ (P ⇒ Q) ∧ (Q ⇒ P).
• De Morgan: ¬(P ∨ Q) ≡ ¬P ∧ ¬Q, en ¬(P ∧ Q) ≡ ¬P ∨ ¬Q.
• Distributie: P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R), met de overeenkomstige omgekeerde wet voor ∧ over ∨.

Conjunctie en disjunctie laten ook hergroepering en verwisseling van de volgorde toe. Deze herschrijvingen leggen de nuttige structuur van een uitspraak bloot zonder een nieuwe feitelijke aanname toe te voegen.

Splits bij B₁₁ ⇔ (P₁₂ ∨ P₂₁) en ¬B₁₁ de bi-implicatie en kies (P₁₂ ∨ P₂₁) ⇒ B₁₁. Contrapositie geeft ¬B₁₁ ⇒ ¬(P₁₂ ∨ P₂₁). Modus ponens levert ¬(P₁₂ ∨ P₂₁) op; De Morgan levert ¬P₁₂ ∧ ¬P₂₁ op. En-eliminatie bewijst vervolgens ¬P₁₂. Het bewijs hoeft nooit elke indeling van de grot op te sommen.

Toets een ongeldige verkorte redenering

Uit P ⇒ Q en Q de uitspraak P afleiden is bevestiging van het gevolg. Uit P ⇒ Q en ¬P de uitspraak ¬Q afleiden is ontkenning van de voorwaarde. Beide gaan niet op in het model P onwaar, Q waar. Een serverstoring kan verhinderen dat een pagina laadt, maar een laadfout heeft ook andere mogelijke oorzaken; de afwezigheid van een storing garandeert evenmin dat het laden lukt.

Een bewijs vinden is een zoekprobleem. De begintoestand bevat de KB; een actie past een afleidingsregel toe en voegt de conclusie toe; de doeltoestand bevat de zoekvraag. De lengte van het bewijs kan als padkosten dienen. Door relevante uitspraken te kiezen, voorkom je dat je moeite steekt in niet-gerelateerde redeneringen. Klassieke logica is monotoon: premissen toevoegen behoudt eerdere logische gevolgen. Standaardregels met uitzonderingen vereisen een andere aanpak, omdat latere informatie een eerdere standaardconclusie kan intrekken.

Resolutie bewijst logisch gevolg door naar een tegenspraak te zoeken. De invoer is conjunctieve normaalvorm (CNF): een EN van clausules, elk een OF van literalen. Een clausule met één literaal is een eenheidsclausule. De lege clausule kan geen ware literaal bevatten en staat voor onwaarheid.

Zet uitspraken om naar clausules

Elimineer eerst ⇔ en ⇒. Verplaats vervolgens negaties naar binnen met de wetten van De Morgan en eliminatie van dubbele negaties. Distribueer ten slotte ∨ over ∧. Een bi-implicatie kan daardoor meerdere clausules opleveren.

Voor B₁₁ ⇔ (P₁₂ ∨ P₂₁) geeft de voorwaartse richting ¬B₁₁ ∨ P₁₂ ∨ P₂₁. De omgekeerde richting geeft ¬(P₁₂ ∨ P₂₁) ∨ B₁₁. De negatie naar binnen verplaatsen en distribueren levert ¬P₁₂ ∨ B₁₁ en ¬P₂₁ ∨ B₁₁ op. Alle drie de clausules zijn nodig voor de volledige bi-implicatie.

Pas resolutie toe op één complementair paar

Uit P ∨ A en ¬P ∨ B leidt resolutie A ∨ B af. Welke waarde P ook heeft, minstens één overgebleven deel moet gelden. Eenheidsresolutie gebruikt een clausule met één literaal: P met ¬P ∨ B levert B op. Dubbele literalen worden weggenomen door factorisatie, zodat resolutie van A ∨ B met A ∨ ¬B de uitspraak A oplevert.

Pas resolutie steeds op precies één complementair paar toe. A ∨ B en ¬A ∨ ¬B zijn samen vervulbaar als A waar en B onwaar is. Beide paren verwijderen zou ten onrechte de lege clausule opleveren. Resolutie op alleen A levert B ∨ ¬B op, een tautologie die geen beperking toevoegt.

Weerleg de ontkende zoekvraag

Om KB ⊨ α te bewijzen, voeg je ¬α toe, zet je de gecombineerde uitspraak om naar CNF en leid je nieuwe resolventen af. Als je de lege clausule bereikt, bewijs je dat er geen tegenmodel bestaat.

Voeg voor de putzoekvraag ¬P₁₂ de uitspraak P₁₂ toe. Pas daarop resolutie toe met ¬P₁₂ ∨ B₁₁ om B₁₁ te krijgen. Pas daarop resolutie toe met de waargenomen ¬B₁₁ om de lege clausule te bereiken. Het bewijs stelt de afwezigheid van de put vast, niet de aanwezigheid ervan: de positieve putliteraal was een tijdelijke ontkende zoekvraag.

Een tweede voorbeeld gebruikt R ⇒ C, (C ∨ I) ⇒ G en R. De CNF-clausules zijn ¬R ∨ C, ¬C ∨ G, ¬I ∨ G en R. Voeg ¬G toe. Resolutie daarvan met ¬C ∨ G geeft ¬C, wat met de eerste clausule ¬R oplevert. Resolutie van ¬R met R voltooit de weerlegging. Er was geen feit over I nodig.

Propositionele resolutie is correct en weerleggingsvolledig. Ze stopt omdat eindig veel symbolen eindig veel verschillende clausules toelaten. Als uitputtende afsluiting geen nieuwe clausule en geen tegenspraak oplevert, volgt de zoekvraag niet logisch. Resolutie hoeft niet elke uitspraak die logisch volgt rechtstreeks af te leiden: uit alleen A construeert resolutie niet A ∨ B.

Distributie kan CNF exponentieel vergroten. Een Tseitin-codering introduceert symbolen voor deelformules en levert CNF van lineaire omvang op. De nieuwe uitspraak is precies dan vervulbaar als de oorspronkelijke; ze hoeft niet logisch equivalent te zijn over het uitgebreide vocabulaire. Behoud van vervulbaarheid is voldoende voor tegenspraaktoetsen met SAT.

Regels met één positieve conclusie maken een eenvoudiger inferentieprocedure mogelijk dan algemene resolutie. Een definiete clausule heeft precies één positieve literaal; ¬A ∨ ¬B ∨ C wordt geschreven als A ∧ B ⇒ C. Een feit heeft een lege romp. Een Hornclausule heeft hoogstens één positieve literaal, waaronder een doelclausule zonder positieve literaal, zoals A ∧ B ⇒ Onwaar.

Laat feiten de regels aansturen

Voorwaarts redeneren begint met bekende feiten. Als elke premisse van een regel bekend is, voeg je de kop toe. Ga door totdat de zoekvraag verschijnt of een vast punt niets toevoegt. Efficiënte implementaties houden een agenda van nieuwe feiten en per regel een teller van nog niet vervulde premissen bij.

Neem StroomAan, VentilatorDraait en BelastingLaag als feiten. De regels zijn StroomAan ∧ VentilatorDraait ⇒ Koeling; Koeling ∧ BelastingLaag ⇒ TemperatuurNormaal; StroomAan ⇒ LedBrandt; LedBrandt ∧ TemperatuurNormaal ⇒ SysteemInOrde; VentilatorDraait ⇒ GeluidHoorbaar. Door StroomAan te verwerken kun je LedBrandt afleiden en wordt gedeeltelijk aan de koelingsregel voldaan. VentilatorDraait maakt Koeling en GeluidHoorbaar mogelijk. Koeling plus BelastingLaag geeft TemperatuurNormaal, waarna TemperatuurNormaal plus LedBrandt SysteemInOrde geeft. GeluidHoorbaar is een geldige extra conclusie, ook al was die voor de zoekvraag niet nodig.

Laat een zoekvraag de regels kiezen

Achterwaarts redeneren begint met SysteemInOrde. De bijbehorende regel vereist LedBrandt en TemperatuurNormaal. LedBrandt wordt herleid tot het bekende StroomAan. TemperatuurNormaal vereist Koeling en BelastingLaag; Koeling vereist StroomAan en VentilatorDraait. Elk blad is een feit, dus slaagt de zoekvraag. De geluidsregel wordt nooit bekeken.

Voor KB's met definiete clausules en atomaire zoekvragen zijn beide methoden met passende zoeksturing correct en volledig. Propositioneel voorwaarts redeneren kan worden uitgevoerd in tijd lineair in de omvang van de KB. Als je in het vaste punt afgeleide symbolen waar maakt en alle andere onwaar, krijg je een model van de definiete clausules.

Handel cycli af zonder antwoorden te verliezen

A ⇒ B en B ⇒ A bezorgen een naïeve achterwaartse procedure een oneindige lus. Een tak kan stoppen wanneer het doel al op de actieve doelstapel staat. Geslaagde subdoelen kunnen worden onthouden, maar een mislukking door een lus is tijdelijk. Met B ⇒ A, A ⇒ B, C ⇒ A en het feit C kan een vroege poging om B te bewijzen mislukken terwijl A actief is. Nadat A uit C is bewezen, slaagt een nieuwe poging voor B. Als je die eerste mislukking permanent onthoudt, gaat het bewijs verloren. Antwoorden opslaan in tabellen houdt afhankelijke doelen bij en bekijkt ze opnieuw wanneer antwoorden verschijnen.

Deze manier van redeneren hangt af van de regelvorm. A ∨ B heeft twee positieve literalen en is dus geen Hornclausule. Samen met A ⇒ C en B ⇒ C volgt daaruit C door beide mogelijkheden te beschouwen. Vanuit alleen de disjunctie wordt geen definiete regel geactiveerd. Algemene resolutie kan deze conclusie bewijzen, ook al loopt eenvoudig voorwaarts of achterwaarts redeneren vast.

Een SAT-oplosser zoekt naar een waardetoekenning die elke clausule in een CNF-uitspraak vervult. Een teruggegeven model kun je rechtstreeks controleren. Een resultaat dat de uitspraak onvervulbaar is, sluit alle waardetoekenningen uit. SAT is NP-volledig, maar gestructureerde probleeminstanties laten vaak veel snellere oplossingen toe dan uitputtende enumeratie met waarheidstabellen.

Verklein de zoekruimte met DPLL

DPLL is diepte-eerst zoeken met backtracking en drie verkortingen. Een ware literaal vervult de hele clausule, terwijl een volledig onware clausule de tak beëindigt. Een zuiver symbool komt onder onvervulde clausules maar met één teken voor en kan dus zo worden ingesteld dat het die voorkomens vervult. Een eenheidsclausule heeft nog maar één mogelijk ware literaal, die waar moet worden gemaakt. Zulke gedwongen keuzes herhalen is eenheidspropagatie.

Neem (A), (¬A ∨ B), (¬B ∨ C ∨ D), (¬C ∨ ¬D), (D ∨ E). E is zuiver, dus maak E waar. De eenheidsclausule A dwingt A waar te zijn, wat B waar dwingt te zijn. De resterende constraint C ∨ D en de clausule ¬C ∨ ¬D vereisen dat precies één van C en D waar is. Vertak op C waar; propagatie dwingt D onwaar te zijn. A, B, C en E waar met D onwaar vervullen elke clausule.

Vertak voor (A ∨ B), (A ∨ ¬B), (¬A ∨ C), (¬A ∨ ¬C) op A. A onwaar dwingt zowel B als ¬B af; A waar dwingt zowel C als ¬C af. Beide takken geven een conflict, dus is de hele uitspraak onvervulbaar.

Leer van conflicten

Conflictgestuurd clausules leren (CDCL) breidt deze zoekmethode uit. Een geleerde clausule blokkeert een combinatie die verantwoordelijk is voor een conflict. Terugspringen slaat irrelevante keuzes over; variabeleactiviteit stuurt de vertakking; herstarts veranderen de zoekroute; bewaakte literalen versnellen propagatie. Geleerde clausules worden door de formule gerechtvaardigd en behouden dus de mogelijke oplossingen ervan.

Zoek door een volledige waardetoekenning te veranderen

WalkSAT begint met een willekeurige volledige waardetoekenning. Het kiest een onvervulde clausule en keert een variabele daarin om, soms willekeurig en soms zo dat de meeste clausules vervuld blijven. Willekeurige stappen helpen om aan lokale valkuilen te ontsnappen. Als in het eerdere voorbeeld alle vijf symbolen onwaar zijn, blijven (A) en (D ∨ E) onwaar. A omkeren herstelt (A), maar maakt (¬A ∨ B) onwaar. Een stap kan de ene clausule herstellen terwijl een andere onwaar wordt.

Geef voor logisch gevolg KB ∧ ¬α als invoer. Onvervulbaarheid bewijst α; een model is een tegenvoorbeeld. Als WalkSAT de tijdslimiet bereikt, blijven beide mogelijkheden open. Bij grote willekeurige 3-CNF-formules ligt een geschatte overgang in de verhouding tussen clausules en variabelen rond 4,26, met vaak moeilijke probleeminstanties in de buurt. Dit is een patroon voor een verzameling formules, geen grens die een afzonderlijke formule beslist. Ook de clausulestructuur en de strategie van de oplosser beïnvloeden de moeilijkheid.

Eerste-ordelogica beschrijft objecten en hun relaties. In plaats van elk vak een niet-gerelateerd symbool te geven, kan ze een regel voor alle vakken uitdrukken: ∀s (Bries(s) ⇔ ∃r (GrenstAan(r, s) ∧ Put(r))). Kwantoren maken algemeenheid onderdeel van de taal.

Onderscheid objecten van beweringen

Een constante benoemt een object, zoals Ada. Een variabele, zoals x, loopt over objecten. Een functie beeldt objecten af op een object: MoederVan(Ada) is een term die naar iemand verwijst. Een predicaat vormt een bewering: Bezit(Ada, Atlas) is waar of onwaar. Een term kan een constante, variabele of op termen toegepaste functie zijn.

Boek(x) is een uitspraak, geen object, dus plaatst Bezit(Ada, Boek(x)) het verkeerde soort uitdrukking op een argumentpositie. Gelijkheid vergelijkt waarnaar termen verwijzen: MoederVan(Ada) = Clara zegt dat beide termen hetzelfde object aanduiden.

Beoordeel een uitspraak in een model

Een eerste-ordemodel levert een niet-leeg domein en een interpretatie. Constanten duiden objecten uit het domein aan, predicaten duiden relaties aan en functies geven uitkomsten voor elk geschikt tupel van objecten uit het domein. Een universeel gekwantificeerde uitspraak moet voor elke mogelijke waarde van de variabele gelden; een existentiële uitspraak heeft minstens één getuige nodig.

Laat het domein {a, b, k} zijn; Ada benoemt a, Ben benoemt b en Atlas benoemt k. Persoon bevat a en b, Boek bevat k en Bezit bevat alleen (a, k). Bezit(Ada, Atlas) is waar. ∃x (Boek(x) ∧ Bezit(Ben, x)) is onwaar omdat Ben geen object bezit. ∀x (Persoon(x) ⇒ ∃y (Boek(y) ∧ Bezit(x, y))) is onwaar omdat Ben een tegenvoorbeeld is. Toch heeft elk boek een eigenaar: ∀x (Boek(x) ⇒ ∃y Bezit(y, x)) geldt.

Maak modelleringsaannamen expliciet

Standaard eerste-ordelogica legt deze databaseaannamen niet op. Boek(Atlas), Boek(Beowulf), Bezit(Ada, Atlas) en Bezit(Ada, Beowulf) laten open of de twee namen hetzelfde boek aanduiden en of Ada meer boeken bezit. Volgens databasesemantiek beschrijven ze precies twee boeken die Ada bezit.

Om die precieze bewering onder standaardsemantiek te krijgen, behoud je de vier feiten en voeg je ¬(Atlas = Beowulf) en ∀x ((Boek(x) ∧ Bezit(Ada, x)) ⇒ (x = Atlas ∨ x = Beowulf)) toe. De ongelijkheid stelt twee verschillende boeken vast; de universele beperking sluit extra boeken in Ada's bezit uit.

Eerste-ordemodellen kunnen willekeurig grote domeinen hebben, dus biedt de eindige enumeratiemethode voor propositionele modellen hier geen algemene beslisprocedure. Bewijsmethoden werken in plaats daarvan met de structuur van de uitspraken. Een vrije variabele heeft voor beoordeling een waardetoekenning nodig; bind variabelen wanneer je een gesloten bewering voor de KB schrijft.

Vertalen begint met bepalen wat de uitspraak over elk object beweert. Het bereik van kwantoren, de richting van implicaties en gelijkheid bepalen de betekenis; predicaatnamen alleen leggen die niet vast. Haakjes maken het bedoelde bereik zichtbaar.

Gebruik het juiste connectief bij een kwantor

“Elke kat is een zoogdier” wordt ∀x (Kat(x) ⇒ Zoogdier(x)). Voor een object buiten de categorie is de implicatie waar zonder dat het een kat is. Als je ∀x (Kat(x) ∧ Zoogdier(x)) schrijft, maak je ten onrechte alles tot een kat.

“Er is een zwarte kat” wordt ∃x (Kat(x) ∧ Zwart(x)). De getuige moet aan beide eigenschappen voldoen. Bij ∃x (Kat(x) ⇒ Zwart(x)) is alles wat geen kat is al een getuige, zelfs in een wereld zonder zwarte katten. Universele categorieregels gebruiken meestal implicatie; existentiële categoriebeweringen gebruiken meestal conjunctie.

Controleer wie van wie kan afhangen

∀x ∃y HoudtVan(x, y) laat voor elke x een andere geliefde persoon toe. ∃y ∀x HoudtVan(x, y) vereist één persoon van wie iedereen houdt. In een wereld met twee personen die elk alleen van de ander houden, geldt de eerste uitspraak en niet de tweede. Het verwisselen van kwantoren van verschillende soorten kan een bewering veranderen; het verwisselen van twee aangrenzende universele kwantoren of twee aangrenzende existentiële kwantoren behoudt die.

Negatie verwisselt kwantoren: ¬∀x P(x) ≡ ∃x ¬P(x), en ¬∃x P(x) ≡ ∀x ¬P(x). Daarom betekent “Niet elke student is geslaagd” hetzelfde als ∃x (Student(x) ∧ ¬Geslaagd(x)). Dat vereist een student die niet is geslaagd; het beweert niet dat elke student niet is geslaagd.

Druk richting en aantal uit

“Alleen leden lenen” betekent ∀x (Leent(x) ⇒ Lid(x)). Lenen is voldoende om lidmaatschap vast te stellen, terwijl lidmaatschap alleen niets zegt over lenen. “Geen reptiel is een zoogdier” betekent ∀x (Reptiel(x) ⇒ ¬Zoogdier(x)).

Om minstens twee boeken in bezit uit te drukken, schrijf je ∃x ∃y (Boek(x) ∧ Boek(y) ∧ Bezit(Ada, x) ∧ Bezit(Ada, y) ∧ ¬(x = y)). De ongelijkheid is van belang: twee variabelenamen kunnen naar hetzelfde object verwijzen. Precies één gebruikt een getuige plus uniciteit: ∃x (Boek(x) ∧ Bezit(Ada, x) ∧ ∀y ((Boek(y) ∧ Bezit(Ada, y)) ⇒ y = x)).

Geef definities beide richtingen

Een definitie van broer of zus kan zijn: ∀x ∀y (BroerOfZus(x, y) ⇔ (¬(x = y) ∧ ∃p (Ouder(p, x) ∧ Ouder(p, y)))). De voorwaartse richting legt beperkingen op aan wie broer of zus is; de omgekeerde maakt het mogelijk om uit feiten over een gedeelde ouder af te leiden dat mensen broer of zus zijn. Een eenzijdige implicatie levert slechts de helft van die betekenis.

In een agentdomein lopen diagnostische regels van waarnemingen naar mogelijke oorzaken, terwijl causale regels van oorzaken naar gevolgen lopen. “Elk vak met een bries heeft een aangrenzende put” is diagnostisch. “Elke put veroorzaakt een bries in elk aangrenzend vak” is causaal. Samen ondersteunen ze de volledige bries-bi-implicatie. Rond een vertaling af door de binding van elke variabele te controleren en een kleine wereld te toetsen waarin de uitspraak in natuurlijke taal onwaar zou moeten zijn.

Een bruikbare kennisbank bouwen is een modelleringstaak. Formele notatie helpt pas nadat de relevante vragen, objecten en relaties zijn gekozen. Kennistechnologie zet die keuzes om in axioma's die je aan de hand van bedoelde voorbeelden kunt controleren.

Bouw rond de vragen

Een praktische volgorde is de taak bepalen, relevante kennis verzamelen, een vocabulaire kiezen, algemene axioma's schrijven, feiten over een specifieke probleemsituatie toevoegen, zoekvragen stellen en fouten in de resultaten opsporen. Begin met concrete vragen zoals “Kan deze student zich voor deze cursus inschrijven?” Die vraag bepaalt wat de representatie moet ondersteunen.

Gebruik voor inschrijving Student(s), Cursus(c), Voorkennis(p, c), Behaald(s, c) en KanInschrijven(s, c). Voorkennis(p, c) betekent dat p vóór c moet zijn behaald; de argumenten omkeren zou de afhankelijkheid omkeren. Een regel is ∀s ∀c ((Student(s) ∧ Cursus(c) ∧ ∀p (Voorkennis(p, c) ⇒ Behaald(s, p))) ⇒ KanInschrijven(s, c)). Die vereist elke vereiste cursus, niet slechts één.

Scheid herbruikbare regels van een probleemsituatie

Stel dat de feiten Student(Mia), Cursus(AI), Voorkennis(Logica, AI), Voorkennis(Programmeren, AI), Behaald(Mia, Logica) en Behaald(Mia, Programmeren) zijn. De algemene regel kan voor andere studenten en cursussen worden hergebruikt, terwijl deze feiten één specifieke situatie beschrijven.

Volgens standaard eerste-ordelogica laten deze feiten extra vereiste cursussen voor AI open. Een passend model kan een niet-behaalde derde vereiste cursus bevatten, dus volgt KanInschrijven(Mia, AI) nog niet logisch. Voeg ∀p (Voorkennis(p, AI) ⇔ (p = Logica ∨ p = Programmeren)) toe om de lijst te voltooien. Nu is elke vereiste cursus een van de twee behaalde cursussen en is de inschrijvingsregel van toepassing. Een database met een gesloten wereld kan hetzelfde antwoord krijgen door ontbrekende feiten over vereiste cursussen als onwaar te behandelen.

Kies wat een object wordt

Een ontologie is het vocabulaire met zijn structurele aannamen. Rood(x) behandelt rood als een eigenschap. Kleur(x, Rood) maakt Rood tot een object, waardoor ∃c (Kleur(x, c) ∧ Kleur(y, c)) een gedeelde kleur kan uitdrukken. Deze stap is reïficatie: ze laat de taal spreken over een eigenschap of categorie als iets op zichzelf.

ASK kan vragen of KanInschrijven(Mia, AI) logisch volgt. ASKVARS kan bindingen voor KanInschrijven(x, AI) opvragen en een substitutie zoals {x/Mia} teruggeven. Dezelfde KB ondersteunt zowel waarheidsvragen als zoekvragen naar passende objecten.

Spoor fouten in betekenis op, niet alleen in syntaxis

Een ontbrekend axioma kan een gewenst logisch gevolg blokkeren; een onjuist axioma kan een ongewenst gevolg ondersteunen. Toets positieve voorbeelden, negatieve voorbeelden en grensgevallen. De regel ∀c (Cursus(c) ⇒ ∃t GeeftLes(t, c)) is te sterk als sommige cursussen nog geen docent hebben. De regel ∀p ∀c (Voorkennis(p, c) ⇒ Behaald(Mia, p)) is te sterk omdat die Mia elke vereiste cursus van elke cursus toekent als behaald.

Predicaatnamen zijn labels voor het redeneersysteem. Een relatie Voorkennis noemen levert op zichzelf geen inschrijvingsbeleid op. De regels moeten feiten over vereiste cursussen, behaalde cursussen en toelating in de bedoelde richting verbinden.

Eerste-orde-inferentie werkt met patronen die variabelen bevatten. Substitutie vervangt variabelen door termen; unificatie vindt vervangingen die twee uitdrukkingen identiek maken. Samen laten ze één algemene regel voor veel specifieke feiten werken zonder eerst elke mogelijke instantie te genereren.

Instantieer gekwantificeerde uitspraken zorgvuldig

Universele instantiatie vervangt een universeel gebonden variabele door een willekeurige gesloten term. Leid uit ∀x (Kat(x) ⇒ Zoogdier(x)) de uitspraak Kat(Tom) ⇒ Zoogdier(Tom) af, of de overeenkomstige instantie met MoederVan(Tom). Een gesloten term bevat geen variabele.

Existentiële instantiatie introduceert een nieuwe naam voor een getuige. Introduceer uit ∃x (Kroon(x) ∧ OpHoofd(x, Jan)) een nieuwe constante C₁ en voeg Kroon(C₁) en OpHoofd(C₁, Jan) toe. In plaats daarvan Ben als getuige noemen zou een niet-gespecificeerd object ten onrechte gelijkstellen aan een bestaand object. De uitgebreide KB behoudt vervulbaarheid, geen equivalentie in het uitgebreide vocabulaire.

Propositionele omzetting genereert gesloten instanties en gebruikt daarna propositioneel redeneren. Functiesymbolen kunnen oneindig veel termen opleveren: Ada, MoederVan(Ada), MoederVan(MoederVan(Ada)), enzovoort. Eerste-ordezoekvragen die logisch volgen, hebben eindige bewijzen, maar een algemene bewijzer kan oneindig blijven draaien als de zoekvraag niet logisch volgt. Dit is semibeslisbaarheid.

Vind een consistente substitutie

Om Kent(Ana, x) met Kent(y, Bo) te unificeren, vergelijk je eerst het predicaat en de ariteit. De eerste argumenten vereisen y = Ana; de tweede vereisen x = Bo. De substitutie {y/Ana, x/Bo} maakt beide uitdrukkingen gelijk aan Kent(Ana, Bo).

Kent(Ana, x) en Kent(y, MoederVan(y)) geven daarentegen {y/Ana, x/MoederVan(Ana)}. Een binding moet in de andere termen worden doorgevoerd. Als dezelfde variabele x in beide uitdrukkingen Kent(Ana, x) en Kent(x, Bo) voorkomt, zou die zowel Ana als Bo moeten worden, zodat syntactische unificatie mislukt.

Variabelen in afzonderlijk gekwantificeerde uitspraken zijn onafhankelijk. Bij variabelen disjunct hernoemen hernoem je ze voordat je uitspraken combineert. Door in dat laatste paar de tweede x te hernoemen tot z wordt {z/Ana, x/Bo} mogelijk. Dit behoudt de bedoelde onafhankelijkheid van de lokale variabelen van twee regels.

Een meest algemene unificator legt geen onnodige bindingen op. Kent(Ana, x) en Kent(y, z) unificeren met {y/Ana, x/z}; ook z gelijkstellen aan Ana zou het resultaat zonder noodzaak specificeren. De voorkomenscontrole verwerpt x = MoederVan(x), omdat een eindige term zichzelf niet kan bevatten. Gewone unificatie in Prolog kan cyclische termen toestaan, dus is voorzichtigheid nodig wanneer eerste-ordelogica met eindige termen is bedoeld.

Pas de overeenkomende regel toe

Gegeneraliseerde modus ponens brengt elke premisse onder één consistente substitutie in overeenstemming. Bezit(Ada, Atlas) en Boek(Atlas) komen overeen met Bezit(x, y) ∧ Boek(y) ⇒ Lezer(x) met {x/Ada, y/Atlas}, wat Lezer(Ada) oplevert. Eén premisse met y = Atlas en een andere met y = Beowulf laten overeenkomen zou de toepassing van de regel niet rechtvaardigen: gedeelde variabelen dwingen gedeelde objecten af.

Een eerste-ordedefiniete clausule heeft atomaire premissen en één atomaire conclusie, waarbij de variabelen als universeel gekwantificeerd worden opgevat. Voorwaarts en achterwaarts redeneren gebruiken unificatie om deze regels op benoemde objecten toe te passen. Datalog behoudt deze regelvorm en sluit functiesymbolen uit, wat in de gebruikelijke situatie met een eindige database een eindige ruimte van mogelijke gesloten feiten oplevert.

Leid bereikbare locaties af

Neem Verbinding(A, B), Verbinding(B, C) en Verbinding(C, D). Gebruik Verbinding(x, y) ⇒ Bereikbaar(x, y) en Verbinding(x, y) ∧ Bereikbaar(y, z) ⇒ Bereikbaar(x, z). In synchrone rondes leest elke regel de feiten die vóór die ronde beschikbaar waren.

Ronde 1 leidt Bereikbaar(A, B), Bereikbaar(B, C) en Bereikbaar(C, D) af. Ronde 2 voegt Bereikbaar(A, C) en Bereikbaar(B, D) toe. Ronde 3 voegt Bereikbaar(A, D) toe. Ronde 4 voegt niets toe. Er zijn zes Bereikbaar-feiten in het vaste punt. Een implementatie die nieuwe feiten direct hergebruikt, kan ze in een andere volgorde vinden, maar bereikt dezelfde afsluiting.

Met n constanten en predicaten met ariteit hoogstens k zijn slechts eindig veel tupels mogelijk; een bovengrens is p · nᵏ voor p predicaten. Daarentegen genereren NatGetal(0) en NatGetal(n) ⇒ NatGetal(S(n)) voortdurend diepere termen. Functiesymbolen nemen de garantie van een eindig domein weg.

Een regel met meerdere premissen met feiten in overeenstemming brengen is een constraintprobleem. Een selectieve premisse kan het aantal substituties dat daarna wordt bekeken sterk verminderen. Incrementeel voorwaarts redeneren richt zich op regels die door nieuw toegevoegde feiten worden beïnvloed. Rete-netwerken bewaren gedeeltelijke overeenkomsten tussen actualisaties, zodat productieregelsystemen werk niet hoeven te herhalen.

Werk achterwaarts met bindingen

Om Bereikbaar(A, D) te bewijzen, probeer je de regel voor directe verbindingen, die het ontbrekende Verbinding(A, D) vereist. De recursieve regel vereist in plaats daarvan Verbinding(A, y) en Bereikbaar(y, D). De eerste bindt y aan B. Als je verdergaat via B en C, bereik je het bekende Verbinding(C, D). De zoekvraag Bereikbaar(A, w) heeft drie antwoorden: w = B, C of D.

Prolog schrijft regels met de kop voorop en gebruikt hoofdletters voor variabelen en kleine letters voor constanten:

reach(X, Y) :- link(X, Y).
reach(X, Z) :- link(X, Y), reach(Y, Z).

Prolog probeert clausules van boven naar beneden en premissen van links naar rechts met diepte-eerst achterwaarts redeneren. Rekenkunde kan N is M + 1 gebruiken. Negatie als falen, geschreven als \+ p, slaagt als de poging om p te bewijzen na eindig veel stappen mislukt. Het is een operationele toets op mislukking, geen algemeen bewijs van klassieke negatie.

Voorkom dat recursie het zoeken vasthoudt

Als je reach(X, Y) voorop in de recursieve romp zet, kan direct hetzelfde onopgeloste doel opnieuw worden aangeroepen. Basisclausules voorop en recursie die een verbinding verwerkt helpen, maar cycli kunnen onsuccesvolle zoekprocedures nog steeds vasthouden. Antwoorden opslaan in tabellen legt antwoorden op subdoelen vast en beheert herhaalde afhankelijkheden. Voorwaarts redeneren is volledig voor eindige Datalog; naïef diepte-eerst achterwaarts zoeken heeft dit soort sturing nodig om bereikbare antwoorden achter oneindige takken niet te missen.

Eerste-orderesolutie breidt redeneren met clausules uit met unificatie. Ze kan conclusies over niet-benoemde objecten bewijzen doordat Skolemtermen de afhankelijkheden van existentiële getuigen behouden. Begin, net als bij propositionele weerlegging, met de KB en de negatie van de zoekvraag.

Bereid eerste-ordeclausules voor

Elimineer ⇔ en ⇒, verplaats negaties naar binnen, hernoem gebonden variabelen, Skolemiseer existentiële variabelen, laat universele kwantoren weg en distribueer daarna ∨ over ∧. Het is van belang eerst de negatie te verplaatsen, omdat ¬∀x P(x) verandert in ∃x ¬P(x), waardoor een ander soort getuige nodig is.

Voor “Elke cursus heeft een docent”, ∀c (Cursus(c) ⇒ ∃t GeeftLes(t, c)), kan de existentiële getuige voor de docent afhangen van c. Introduceer een nieuwe functie T(c) om ¬Cursus(c) ∨ GeeftLes(T(c), c) te krijgen. Eén constante zou één gemeenschappelijke docent opleggen, wat de oorspronkelijke uitspraak niet vereist. Voor ∃t ∀c (Cursus(c) ⇒ GeeftLes(t, c)) is een nieuwe constante passend, omdat de getuige aan de universele kwantor voorafgaat.

“Niet elke vogel vliegt” wordt ∃x (Vogel(x) ∧ ¬Vliegt(x)), vervolgens Vogel(B₁) en ¬Vliegt(B₁). Beide clausules gebruiken dezelfde nieuwe getuige. Skolemisatie behoudt vervulbaarheid; het is geen gewone equivalentie over het uitgebreide vocabulaire.

Pas een unificator toe op de hele resolvent

Hernoem de variabelen van de twee clausules disjunct. Zoek complementaire literalen die unificeren, verwijder ze en pas hun meest algemene unificator toe op elke overgebleven literaal. Factorisatie voegt ook unificeerbare literalen binnen een clausule samen. Resolutie met factorisatie is weerleggingsvolledig voor eerste-ordeclausules.

Neem ¬Cursus(c) ∨ GeeftLes(T(c), c), ¬GeeftLes(u, v) ∨ Medewerker(u) en Cursus(Logica). De zoekvraag is ∃w Medewerker(w); de negatie ervan geeft ¬Medewerker(w), universeel gekwantificeerd. Pas resolutie toe op het cursusfeit en de eerste clausule om GeeftLes(T(Logica), Logica) te krijgen. Resolutie met de tweede clausule onder {u/T(Logica), v/Logica} geeft Medewerker(T(Logica)). Resolutie met ¬Medewerker(w) onder {w/T(Logica)} levert de lege clausule op. Er bestaat een medewerker, hoewel de KB die persoon nooit een gewone naam geeft.

Stuur het zoeken naar clausules

Voorkeur voor eenheidsclausules kiest eerst korte clausules. De ondersteuningsverzameling vereist een ouderclausule uit de ontkende zoekvraag of uit de afstammelingen daarvan en behoudt volledigheid wanneer de resterende KB vervulbaar is. Invoerresolutie vereist bij elke stap een oorspronkelijke ouderclausule en is volledig voor Horn-KB's. Subsumptie verwijdert een zwakkere clausule die al door een sterkere algemene clausule wordt gedekt, zoals P(Ana) ∨ Q(Bo) verwijderen wanneer P(x) bekend is.

Gelijkheid vereist een specifieke behandeling: gelijkheidsaxioma's, herschrijven met vergelijkingen door demodulatie of afleidingen zoals paramodulatie. Zuiver syntactische resolutie alleen omvat niet elke betekenis van gelijkheid. Een eerlijke volledige zoekprocedure vindt voor elke onvervulbare eerste-ordeclausuleverzameling een tegenspraak, maar kan anders oneindig doorgaan. Voorbeelden van bewijzers op basis van resolutie zijn Vampire en E; EQP bewees het vermoeden van Robbins in 1996.

Een ontologie ordent de categorieën, objecten, relaties en aannamen van een domein. Een bovenliggende ontologie levert algemene begrippen zoals objecten, gebeurtenissen en tijd; een domeinontologie levert de onderscheidingen die in een bepaald vakgebied nuttig zijn. Klinische en biologische ontologieën laten zien waarom een bruikbaar gemeenschappelijk vocabulaire vaak een specifieke gemeenschap dient.

Houd lidmaatschap en subklasse gescheiden

Een categorie kan voorkomen als predicaat, Laptop(x), of als object, Laptops. Lidmaatschap x ∈ Laptops zegt dat een individu ertoe behoort. Laptops ⊂ Computers zegt dat elke laptop een computer is. Een taxonomie ordent zulke subklasserelaties in een hiërarchie. Als elke computer een processor heeft, erven laptops die eigenschap.

De subklasserelatie is transitief: Pinguïns ⊂ Vogels en Vogels ⊂ Dieren geven Pinguïns ⊂ Dieren. Lidmaatschap is niet transitief. Pingu ∈ Pinguïns en Pinguïns ∈ Soorten maken Pingu niet tot een soort. De ene uitspraak gaat over een individuele vogel; de andere gaat over een categorie die als object wordt behandeld.

Categorieën zijn disjunct als ze geen leden delen. Een uitputtende decompositie omvat elk lid van de bovenliggende categorie. Een partitie doet beide: negatieve gehele getallen, nul en positieve gehele getallen vormen een partitie van de gehele getallen. Uitputtendheid laat overlap toe, tenzij ook disjunctheid is vermeld.

Geef onderdelen, gebeurtenissen en overgeërfde waarden weer

DeelVan beschrijft samenstelling, geen categorielidmaatschap. DeelVan is transitief: een spaak die bij een wiel hoort dat bij een fiets hoort, is onderdeel van de fiets. Een fiets is daarmee geen soort wiel. Gebeurtenissen kunnen ook objecten zijn: Gebeurt(e, t), Initieert(e, f, t) en GeldtOp(f, t) verbinden gebeurtenissen met veranderlijke toestandsuitspraken. Een lamp inschakelen initieert een veranderlijke toestandsuitspraak die blijft gelden totdat een gebeurtenis die beëindigt.

Een semantisch netwerk tekent objecten en categorieën als knopen met gelabelde relaties. In een netwerk met standaardveronderstellingen kan “vogels vliegen normaal gesproken” een waarde leveren die gewone vogels erven, terwijl een specifiekere pinguïncategorie die waarde vervangt. Dit verschilt van het vastleggen van het uitzonderingsloze klassieke axioma ∀x (Vogel(x) ⇒ Vliegt(x)), dat ook voor pinguïns zou gelden.

Kies de redeneertaal

Beschrijvingslogica's ondersteunen subsumptie, classificatie en consistentiecontroles. Een definitie kan een persoon met minstens drie kinderen in een passende categorie indelen. Deze logica's vormen de basis van de beschrijvingslogicatalen van OWL.

Redeneren met standaardveronderstellingen is niet-monotoon: als je leert dat een vogel een pinguïn is, kan de standaardconclusie dat die vliegt worden ingetrokken. Circumscriptie minimaliseert afwijkende gevallen in regels zoals Vogel(x) ∧ ¬Afwijkend(x) ⇒ Vliegt(x). Standaardlogica staat conclusies toe zolang ze consistent blijven met de kennis. Waarheidsonderhoudssystemen leggen onderbouwing vast, zodat conclusies die afhangen van een ingetrokken overtuiging kunnen worden verwijderd.

Een kennisgraaf slaat entiteiten en hun relaties op als een gerichte graaf. Een eenvoudige verbinding wordt een tripel: subject, predicaat, object. Bijvoorbeeld (Ada, werktBij, Lab) komt overeen met WerktBij(Ada, Lab); (Ada, type, Onderzoeker) geeft categorielidmaatschap aan. Een schema geeft deze labels een gemeenschappelijke betekenis en maakt verdere inferentie mogelijk.

Onderscheid de webstandaarden

RDF geeft grafen weer als tripels. Subjecten zijn IRI's of anonieme knopen, predicaten zijn IRI's en objecten kunnen ook letterlijke waarden zijn. IRI's identificeren bronnen over datasets heen; een anonieme knoop vertegenwoordigt een bron zonder die een globale identificator te geven. RDFS voegt klassen, subklasserelaties en het domein en bereik van eigenschappen toe. OWL biedt uitgebreidere ontologiedefinities. SPARQL vergelijkt graafpatronen om variabelenbindingen terug te geven. Eigenschapsgrafen bieden een ander model met sleutel-waarde-eigenschappen op knopen en verbindingen; Cypher en GQL zijn zoektalen voor die familie.

Als Ada als Onderzoeker is getypeerd en Onderzoeker een subklasse van Wetenschapper is, leidt een subklasseregel af dat Ada een Wetenschapper is. Dit is eerste-ordevoorwaarts redeneren met Lid(x, c) ∧ Deelverzameling(c, d) ⇒ Lid(x, d). Een zoekmachine voor grafen heeft de relevante ondersteuning voor logisch gevolg of opgeslagen afgeleide conclusies nodig om dit afgeleide feit zichtbaar te maken.

Vergelijk een zoekvraag en behoud details

Als ex: als IRI-voorvoegsel is gedeclareerd, kan een zoekvraag zijn:

SELECT ?p WHERE {
  ?p a ex:Researcher .
  ?p ex:worksAt ex:Lab .
}

Dezelfde ?p moet aan beide patronen voldoen. Het is een koppeling, geen twee afzonderlijke zoekopdrachten. Resultaten zijn bindingen zoals ?p = ex:Ada, net als substituties in logische zoekvragen.

Een binaire verbinding kan niet op zichzelf elke rol in een gebeurtenis met een datum uitdrukken. Maak voor een prijs een gebeurtenis- of uitspraaksknoop en verbind die met de ontvanger, prijs en het jaar. Dit houdt de details van één prijs bij elkaar en voorkomt dat je de datum per ongeluk aan elke prijs van dat type koppelt. Wikidata ondersteunt uitspraakkwalificaties voor zulke details.

Onderscheid ontbrekende, afgeleide en voorspelde verbindingen

RDF en OWL gebruiken een openwereldinterpretatie: een ontbrekende verbinding naar een echtgenoot laat de relatie onbekend. Toepassingen met een gesloten wereld maken een andere keuze over ontbrekende feiten. Een leeg zoekresultaat meldt dat er onder die zoekinstellingen geen overeenkomst is; het stelt op zichzelf geen universeel negatief feit vast.

Wikidata, DBpedia, Google's Knowledge Graph en interne organisatiegrafen ondersteunen feitelijke zoekvragen, gegevenskoppeling, aanbevelingen en het ophalen van informatie voor generatieve systemen. Hun feiten kunnen onvolledig of verouderd zijn. Entiteitsresolutie herkent gegevens die naar hetzelfde verwijzen, ook wanneer identificatoren verschillen.

Vectorinbeddingen kennen vectoren toe aan entiteiten en relaties. In TransE wordt de beginvector plus de relatievector zo getraind dat die dicht bij de eindvector ligt. Een hoge score suggereert een ontbrekende verbinding; het is een statistische voorspelling. Logische inferentie leidt een gevolg af uit vastgelegde feiten en regels. Houd dit verschil zichtbaar wanneer je beslist of een nieuwe verbinding bij geverifieerde feiten hoort.

Klassieke planning zoekt acties die een bekende begintoestand naar een doel leiden. Het model is volledig waarneembaar, deterministisch en discreet en bevat één agent; de wereld verandert door de gemodelleerde acties. Een gefactoriseerde representatie beschrijft elke toestand met veranderlijke toestandsuitspraken, zodat een planner kan redeneren over wat elke actie verandert.

Schrijf de toestand en actieschema's op

In het basisfragment van PDDL in STRIPS-stijl vermeldt een toestand ware gesloten atomaire veranderlijke toestandsuitspraken. Niet-vermelde veranderlijke toestandsuitspraken zijn volgens de geslotenwereldaanname onwaar. Het herbruikbare domein declareert predicaten en actieschema's; het probleem declareert objecten, de begintoestand en een doel. PDDL werd voor de planningswedstrijd van 1998 geïntroduceerd en bouwde voort op STRIPS.

Een actieschema heeft parameters, een voorwaarde vooraf en effecten. Ga(r, van, naar) vereist Op(r, van) en Verbonden(van, naar); het voegt Op(r, naar) toe en verwijdert Op(r, van). Pak(r, p, l) vereist Op(r, l), In(p, l) en HandLeeg(r); het voegt Vast(r, p) toe en verwijdert In(p, l) en HandLeeg(r). ZetNeer vereist de locatie en het vasthouden; het voegt de locatie van het pakket en een lege hand toe en verwijdert het vasthouden.

Een gesloten actie is alleen toepasbaar wanneer haar voorwaarden vooraf gelden. De actualisatie is RESULT(s, a) = (s − DEL(a)) ∪ ADD(a). Andere veranderlijke toestandsuitspraken blijven gelden, waaronder statische Verbonden-feiten. Dit impliciete behoud behandelt het frameprobleem zonder een apart axioma voor elke onveranderde toestandsuitspraak.

Volg een bezorging in vier acties

Aanvankelijk is R op het Laadperron, staat Doos bij Stelling en is de hand van R leeg. Verbonden-verbindingen verbinden Laadperron met Stelling en Stelling met Inpakplek in beide richtingen. Het doel is In(Doos, Inpakplek).

1. Ga(R, Laadperron, Stelling) verandert de locatie van R en behoudt de feiten over de doos en de hand.
2. Pak(R, Doos, Stelling) verwijdert de doos van de stelling en zorgt dat R die vasthoudt.
3. Ga(R, Stelling, Inpakplek) verplaatst R en behoudt Vast(R, Doos).
4. ZetNeer(R, Doos, Inpakplek) plaatst de doos bij Inpakplek en maakt de hand vrij.

Het doel laat de eindlocatie van de robot ongespecificeerd, behalve waar de acties die vereisen. Doelen beschrijven doorgaans veel aanvaardbare toestanden, niet één volledige toestand.

Lees en controleer een schema

(:action pick
 :parameters (?r ?p ?l)
 :precondition (and (at ?r ?l) (in ?p ?l) (hand-empty ?r))
 :effect (and (holding ?r ?p)
              (not (in ?p ?l)) (not (hand-empty ?r))))

Een verwijderingseffect weglaten kan een robot op twee plaatsen achterlaten of een pakket zowel vastgehouden als op een stelling. Een vereiste voorwaarde alleen in een effect opnemen zorgt dat de actie die voorwaarde creëert in plaats van controleert.

In de blokkenwereld vereist het verplaatsen van een vrij blok b van x naar een vrij blok y de uitspraken Op(b, x), Vrij(b), Vrij(y), Blok(b), Blok(y) en ¬(b = y). De actie voegt Op(b, y) en Vrij(x) toe en verwijdert Op(b, x) en Vrij(y). De controles op onderscheid en blokken voorkomen dat een blok op zichzelf wordt gestapeld en dat de tafel als één blok wordt behandeld. Een afzonderlijke actie VerplaatsNaarTafel houdt de tafel beschikbaar voor andere blokken.

Een planningsmodel definieert een zoekruimte, maar nuttige acties kiezen blijft moeilijk. Voorwaarts plannen zoekt voorwaarts door volledige toestanden. Regressie zoekt achterwaarts door de voorwaarden waaraan een voorafgaande toestand moet voldoen. Beide kunnen algemene zoekmethoden hergebruiken en tegelijk de actiestructuur benutten.

Zoek vanaf beide kanten

Voorwaarts plannen begint bij de begintoestand en past toepasbare gesloten acties toe. Het kan moeite verspillen aan irrelevante acties: één robot, 20 dozen en 10 locaties geven al 200 mogelijke gesloten Pak-combinaties voordat op toepasbaarheid wordt gefilterd.

Regressie beschouwt een actie die een doelliteraal bereikt zonder een andere doelliteraal te ontkennen. Pas regressie toe op een doelverzameling g door a door bereikte literalen te verwijderen en voorwaarden vooraf toe te voegen: g′ = (g − EFFECT(a)) ∪ PRECOND(a). EFFECT bevat positieve en negatieve literalen met hun teken. Verwerp een inconsistent resultaat dat een literaal en de negatie ervan bevat.

Voor In(Doos, Inpakplek) ∧ Op(R, Laadperron) geeft regressie door ZetNeer(R, Doos, Inpakplek) de uitspraak Vast(R, Doos) ∧ Op(R, Inpakplek) ∧ Op(R, Laadperron). Deze voorwaarden zijn in strijd met de bedoelde invariant dat de robot zich op één locatie bevindt. Een geldig plan moet de doos bezorgen voordat de robot definitief terugkeert. Regressie door Ga(R, Stelling, Laadperron) geeft daarentegen In(Doos, Inpakplek) ∧ Op(R, Stelling) ∧ Verbonden(Stelling, Laadperron), waarbij het bezorgde pakket behouden blijft.

Schat de afstand met eenvoudigere problemen

Een heuristiek is toelaatbaar wanneer ze de resterende optimale kosten nooit overschat. A* met een toelaatbare heuristiek vindt een optimaal plan. Onvervulde doelen tellen is niet altijd toelaatbaar: één actie kan meerdere doelen bereiken.

Voorwaarden vooraf negeren maakt alle acties direct bruikbaar. Verwijderingseffecten negeren maakt vooruitgang blijvend, voor problemen die met positieve voorwaarden vooraf en doelen zijn uitgedrukt. Negatieve voorwaarden moeten eerst worden omgezet in expliciet bijgehouden positieve veranderlijke toestandsuitspraken. De optimale gerelaxeerde planlengte h⁺ is een ondergrens voor de werkelijke planlengte, maar de berekening ervan is NP-moeilijk. FF vindt snel een gerelaxeerd plan zonder de optimaliteit ervan te garanderen; de lengte kan h⁺ overschatten en is niet gegarandeerd toelaatbaar.

Voor het doel van magazijnbezorging plus terugkeer heeft het werkelijke kortste plan zes acties: ga naar Stelling, pak de doos, ga naar Inpakplek, zet de doos neer, keer terug naar Stelling en keer terug naar Laadperron. De relaxatie zonder verwijderingseffecten heeft alleen de eerste vier nodig, omdat Op(R, Laadperron) waar blijft na vertrek. Dus h⁺ = 4 terwijl de werkelijke kosten 6 zijn. Het aantal onvervulde doelen begint bij slechts 1 en mist het grootste deel van dat werk.

Combineer schattingen zonder dubbel te tellen

Een planningsgraaf wisselt niveaus met mogelijke veranderlijke toestandsuitspraken en acties af, met verbindingen voor wederzijdse uitsluiting die onverenigbare paren markeren. Het eerste verschijnen van een doel geeft een niveauschatting. Het maximum van afzonderlijke doelniveaus nemen is toelaatbaar; ze optellen kan gedeeld werk herhaaldelijk meetellen. Toestandsabstractie verwijdert sommige veranderlijke toestandsuitspraken om de toestandsruimte te verkleinen. Ook bij deeldoeldecompositie helpt het om gedeelde acties te controleren: het maximum van toelaatbare deeldoelkosten is veilig, terwijl hun som extra onderbouwing vereist.

Planningsmethoden verschillen in wat ze doorzoeken: toestanden, waardetoekenningen, ordeningsconstraints of verfijningen van procedures van experts. Hun bruikbaarheid hangt af van interactie tussen deeldoelen en de aannamen die het model over de uitvoering maakt.

Herken samenwerkende en conflicterende deeldoelen

In de Sussman-anomalie ligt C op A, terwijl A en B op de tafel staan. Het doel is Op(A, B) ∧ Op(B, C). Eerst het deeldoel A-op-B voltooien blokkeert de latere plaatsing van B. B direct op C plaatsen laat A ingesloten achter. Een kortste plan maakt eerst A vrij en bouwt daarna de stapel van onderaf op: verplaats C naar de tafel, verplaats B op C en verplaats daarna A op B. De drie verplaatsingen verweven voorbereiding en het bereiken van doelen.

Codeer een begrensd plan als SAT

SATPlan kiest een horizon T. Het stelt veranderlijke toestandsuitspraken aan het begin op tijdstip 0, doeluitspraken op T, voorwaarden vooraf voor acties, opvolgertoestandsconstraints en uitsluitingen voor onverenigbare acties. Een vervullende waardetoekenning selecteert acties die een plan vormen. Een onvervulbaar resultaat sluit plannen binnen die codering en horizon uit.

Horizonten op volgorde proberen vindt de kleinste vervulbare horizon. Bij parallelle acties minimaliseert dit het aantal lagen, niet noodzakelijk het totale aantal acties. Er is een stopgrens nodig om uit herhaaldelijk onvervulbare horizonten te kunnen concluderen dat er geen plan bestaat.

Houd alleen de noodzakelijke volgorde aan

Planning met partiële ordening legt acties, ordeningsconstraints en causale koppelingen vast. Een koppeling A -p→ B zegt dat A voorwaarde vooraf p voor B tot stand brengt. Een actie C die p daartussen zou kunnen verwijderen, is een bedreiging. Demotie plaatst C vóór A; promotie plaatst C na B. Niet-gerelateerde acties kunnen tot de uitvoering ongeordend blijven, volgens het principe om zo weinig mogelijk vast te leggen.

HTN-planning verfijnt taken op hoog niveau via een verzameling methoden. BezorgDoos kan worden: reis naar de doos, pak die op, reis naar de bestemming en zet die neer. Deze methoden coderen procedures van experts, zodat het zoeken zich kan richten op nuttige verfijningen in plaats van op elk punt elke primitieve actie te beschouwen.

Stem het model af op de wereld

Het bestaan van een plan voor algemeen propositioneel STRIPS is PSPACE-volledig. De blokkenwereld heeft voor mogelijke rangschikkingen een eenvoudiger bestaansprobleem: verplaats de blokken naar de tafel en bouw opnieuw op, met hoogstens 2n verplaatsingen voor n blokken. Een kortste plan voor de blokkenwereld vinden is nog steeds NP-moeilijk.

Klassieke modellen laten onzekere uitkomsten, verborgen toestand en de duur van acties buiten beschouwing. Sensorloze plannen werken zonder waarnemingen, conditionele plannen vertakken op basis van waarnemingen, online herplanning reageert op verschillen tijdens de uitvoering en tijdsplanning behandelt tijden en middelen. Een ontbrekende voorwaarde vooraf voor de batterij kan een plan dat in het model geldig is in de werkelijkheid laten mislukken. Bewaking van de uitvoering controleert deze kloof. Automatische planning heeft echte systemen bereikt, waaronder NASA's Remote Agent op Deep Space 1 in 1999.