Logische Agenten und Planung

Ein wissensbasierter Agent handelt auf Grundlage einer Beschreibung seiner Welt. Seine Wissensbasis (KB) enthält formale Sätze: anfängliche Fakten und Regeln, die Axiome heißen, sowie Informationen, die während des Betriebs hinzugefügt werden. Inferenz verbindet diese Sätze mit Schlussfolgerungen, die der Agent nie direkt beobachtet hat.

Verbinde Wahrnehmung mit Aktion

TELL fügt der KB einen Satz hinzu. ASK fordert eine durch die KB gestützte Antwort an, die entweder bereits gespeichert ist oder abgeleitet wird. In jedem Zeitschritt hält der Agent seine Wahrnehmung fest, fragt, welche Aktion er ausführen soll, hält die gewählte Aktion fest und führt sie aus. Das Festhalten von Aktionen ist wichtig, weil der Agent beim späteren Schlussfolgern wissen muss, wie sich die Welt verändert hat.

Auf der Wissensebene könnten wir sagen, dass ein Roboter weiß, dass ein Durchgang blockiert ist, und einen Lagerbereich erreichen will. Auf der Implementierungsebene beschreiben wir Datenstrukturen und Inferenzverfahren. Ein deklarativer Entwurf liefert Fakten und Regeln; ein prozeduraler Entwurf schreibt Verhalten direkt in Code. Ein funktionsfähiger Agent kann beides verbinden.

Interpretiere die Wumpus-Welt

Die Wumpus-Welt ist ein 4 × 4-Raster. Koordinaten werden als [Spalte, Zeile] angegeben; der Agent startet bei [1, 1] mit Blickrichtung nach rechts. Es gibt einen Wumpus, ein Stück Gold und auf jedem Feld außer dem Startfeld eine Grubenwahrscheinlichkeit von 0,2. Gruben und Wumpus bleiben an ihrem Platz. Die Welt ist diskret, deterministisch und enthält einen einzelnen Agenten, ist aber partiell beobachtbar: Die Anordnung ist verborgen.

Ein Lufthauch weist auf eine Grube in einem direkt benachbarten Feld hin; Gestank weist dort auf den Wumpus hin. Diagonale Felder zählen nicht. Glitzern zeigt Gold auf dem aktuellen Feld an, ein Stoß meldet eine Wand und ein Schrei meldet den Tod des Wumpus von jedem Ort in der Höhle aus. Die Aktionen sind Vorwärtsgehen, Linksdrehen, Rechtsdrehen, Greifen, Schießen und Heraussteigen. Der Agent hat einen Pfeil; das Heraussteigen ist nur von [1, 1] aus möglich. Das Verlassen der Höhle mit Gold bringt 1000 Punkte, der Tod kostet 1000, jede Aktion kostet 1 und das Schießen weitere 10.

Kombiniere Beobachtungen

Bei [1, 1] schließt das Fehlen eines Lufthauchs Gruben in [1, 2] und [2, 1] aus; der fehlende Gestank schließt dort den Wumpus aus. Beide Felder sind sicher. Bei [2, 1] weist ein Lufthauch auf eine Grube in [2, 2] oder [3, 1] hin, weil das Startfeld keine enthält. Der fehlende Gestank schließt den Wumpus in [2, 2] und [3, 1] aus.

Der Agent besucht als Nächstes [1, 2]. Dort schließt der fehlende Lufthauch eine Grube in [2, 2] aus, sodass aus der früheren Disjunktion zwingend eine Grube in [3, 1] folgt. Gestank bei [1, 2] zeigt an, dass der Wumpus in [1, 3] oder [2, 2] ist. Die frühere Beobachtung ohne Gestank schließt [2, 2] aus, sodass [1, 3] übrig bleibt. Der Agent hat festgestellt, dass [2, 2] keine der beiden Gefahren enthält, ohne das Feld zu betreten.

Dieses Schlussfolgern hängt sowohl von den Wahrnehmungen als auch von den Regeln ab, die Wahrnehmungen mit Gefahren verbinden. Ein unerforschtes Feld ist unbekannt, wenn die KB weder Sicherheit noch Gefahr stützt. Dass sich eine Gefahr nicht ableiten lässt, reicht nicht aus, um Sicherheit zu behaupten. Die Entscheidung, ein solches Feld zu betreten, erfordert eine Risikobewertung, die über die logischen Folgerungen allein hinausgeht.

Die Aussagenlogik gibt einem Agenten präzise Regeln, um Aussagen mit Ja-Nein-Antworten zu verknüpfen. Ein atomares Symbol bezeichnet eine vollständige Aussage, etwa P₁₂ für „In [1, 2] liegt eine Grube“. Ein Literal ist ein Atom oder seine Negation. Größere Sätze verbinden diese mit ¬, ∧, ∨, ⇒ und ⇔.

Werte die Junktoren aus

Ein Modell weist jedem Symbol wahr oder falsch zu. Bei n Symbolen gibt es 2ⁿ Belegungen. Eine Negation kehrt einen Wahrheitswert um; eine Konjunktion verlangt, dass beide Seiten wahr sind; eine einschließende Disjunktion verlangt mindestens eine wahre Seite. Eine Implikation ist nur bei wahrer Voraussetzung und falscher Schlussfolgerung falsch. Eine Äquivalenz verlangt auf beiden Seiten gleiche Wahrheitswerte.

Die Bindungsreihenfolge ist ¬, ∧, ∨, ⇒, ⇔. Somit bedeutet ¬A ∧ B ⇒ C dasselbe wie ((¬A) ∧ B) ⇒ C. Verwende Klammern, wenn die beabsichtigte Gruppierung unklar sein könnte. Bei A wahr, B falsch und C wahr ist (A ∨ B) ⇒ C wahr, während A ⇒ (B ∧ C) falsch ist.

Eine logische Implikation legt eine Bedingung für Wahrheitswerte fest, keine Ursache. Eine falsche Voraussetzung macht die Implikation wahr. Sie erlaubt es auch nicht, die Richtung umzukehren: Aus „Wenn der Akku leer ist, hält der Roboter an“ lässt sich allein aus dem Anhalten nicht auf einen leeren Akku schließen.

Kodiere beide Richtungen einer Regel

Die Lufthauchregel am Start lautet B₁₁ ⇔ (P₁₂ ∨ P₂₁). Sie besagt, dass genau dann ein Lufthauch auftritt, wenn eine benachbarte Grube existiert. Die Richtung B₁₁ ⇒ (P₁₂ ∨ P₂₁) ermöglicht es, aus einem Lufthauch auf eine Gefahr zu schließen. Die umgekehrte Richtung ermöglicht es, aus dem Fehlen eines Lufthauchs Gruben auszuschließen. Lässt man sie weg, entfällt die Schlussfolgerung von ¬B₁₁ auf ¬P₁₂ ∧ ¬P₂₁.

Jedes Feld benötigt seine eigene aussagenlogische Regel. Um genau einen Wumpus unter 16 Feldern zu kodieren, braucht man eine Disjunktion für mindestens einen sowie für jedes Paar eine Bedingung für höchstens einen. Es gibt 16 × 15 / 2 = 120 verschiedene Paare. Aussagenlogische Symbole können nicht über Felder quantifizieren, sodass allgemeine Regeln zu vielen einzelnen Sätzen werden.

Stelle Veränderung dar, ohne das Fortbestehen zu verlieren

Ein Fluent ist ein Fakt, dessen Wahrheitswert sich ändern kann. Eine hochgestellte Zeitangabe unterscheidet seine Werte: L₁₁⁰ hält den Ort zum Zeitpunkt 0 fest. Ein Effektaxiom kann besagen, dass eine Bewegung nach rechts von [1, 1] zum Ort [2, 1] zum Zeitpunkt 1 führt und den alten Ort aufhebt. Es lässt offen, was mit unabhängigen Fakten geschieht, etwa dem Besitz des Pfeils. Alle diese unveränderten Fakten zu beschreiben, ist das Rahmenproblem.

Ein Nachfolgezustandsaxiom liefert pro Fluent eine vollständige Aktualisierungsregel: Fᵗ⁺¹ ⇔ (eine Aktion macht F wahr) ∨ (Fᵗ ∧ keine Aktion macht F falsch). Für den Pfeil gilt HaveArrowᵗ⁺¹ ⇔ (HaveArrowᵗ ∧ ¬Shootᵗ). Da keine Aktion einen weiteren Pfeil liefert, bleibt er bis zum Schießen vorhanden und danach nicht mehr vorhanden.

Ein Agent braucht einen Maßstab, um zu entscheiden, ob eine Schlussfolgerung gerechtfertigt ist. Logische Folgerung, geschrieben KB ⊨ α, bedeutet, dass α in jedem Modell wahr ist, das die KB erfüllt. Eine einzige damit vereinbare Welt, in der α falsch ist, widerlegt die logische Folgerung.

Behalte genau die vereinbaren Modelle

Die Modellprüfung zählt Belegungen auf, verwirft diejenigen, die einen KB-Satz falsch machen, und prüft die Anfrage in den übrigen. Angenommen, die KB enthält A ∨ B und ¬A. Von den vier Belegungen für A und B erfüllt nur A falsch, B wahr beide Sätze. Aus der KB folgen B und ¬A. A folgt nicht, weil es im verbleibenden Modell falsch ist.

In der Wumpus-KB verwenden ¬P₁₁, B₁₁ ⇔ (P₁₂ ∨ P₂₁), B₂₁ ⇔ (P₁₁ ∨ P₂₂ ∨ P₃₁), ¬B₁₁ und B₂₁ sieben Symbole. Es gibt 128 Belegungen. Genau drei erfüllen die KB: P₁₂ und P₂₁ sind falsch, während P₂₂ und P₃₁ jeweils wahr/falsch, falsch/wahr oder wahr/wahr sind. Somit folgt ¬P₁₂. P₂₂ variiert zwischen den drei Modellen, also folgt weder P₂₂ noch ¬P₂₂. Diese Grubenregeln allein belegen das Fehlen einer Grube, nicht das Fehlen des Wumpus.

Unterscheide die wichtigsten logischen Prüfungen

P ∨ ¬P ist allgemeingültig; P ∧ ¬P ist unerfüllbar. P ⇒ Q und ¬P ∨ Q sind äquivalent. Äquivalenz setzt logische Folgerung in beide Richtungen voraus. Aus A ∧ B folgt A, aber A erlaubt Modelle, in denen B falsch ist, sodass die umgekehrte Folgerung nicht gilt.

Wandle eine Anfrage in eine Widerspruchsprüfung um

KB ⊨ α gilt genau dann, wenn KB ∧ ¬α unerfüllbar ist. Durch Hinzufügen der negierten Anfrage sucht man nach einer Welt, in der die KB gilt und die Anfrage falsch ist. Findet man keine, beweist das die logische Folgerung; findet man eine, erhält man ein Gegenmodell. Gleichbedeutend gilt α ⊨ β genau dann, wenn α ⇒ β allgemeingültig ist. Die Allgemeingültigkeit von α selbst lässt sich prüfen, indem man untersucht, ob ¬α unerfüllbar ist.

Der Junktor ⇒ gehört in einen Satz. Das Symbol ⊨ beschreibt eine Beziehung zwischen Sätzen und ihren Modellen. Ebenso kann „folgt nicht“ bedeuten, dass die Anfrage ausgeschlossen ist oder unbekannt bleibt. Prüfe, ob die Negation folgt, bevor du zwischen beiden Fällen entscheidest.

Aufzählung ist für die Aussagenlogik korrekt und vollständig, weil sie eine endliche Menge vollständig prüft. Tiefenzuerst ausgeführte Aufzählung benötigt O(2ⁿ) Zeit und O(n) Speicher; schon 50 Symbole ergeben etwa 1,13 × 10¹⁵ Belegungen. Aussagenlogische Folgerung ist co-NP-vollständig. Prüfe auch die Konsistenz: Aus einer KB ohne Modelle folgt jeder Satz, weil sie kein vereinbares Modell hat, das irgendeine Anfrage verletzen könnte.

Ein Beweis leitet eine Anfrage ab, indem er Regeln auf bereits bekannte Sätze anwendet. KB ⊢ α hält eine Ableitung fest; KB ⊨ α eine semantische Aussage über Modelle. Ein korrektes Beweisverfahren verbindet beides: Jede abgeleitete Schlussfolgerung folgt tatsächlich. Ein vollständiges Verfahren kann innerhalb seiner vorgesehenen Sprache jede logisch folgende Schlussfolgerung ableiten.

Wende Regeln auf ihre Prämissen an

Modus ponens führt von P ⇒ Q und P zu Q. Und-Elimination führt von P ∧ Q zu einem der beiden Konjunkte. Sind SensorOn ∧ Calibrated und SensorOn ⇒ ReadingAvailable bekannt, ergibt die Und-Elimination SensorOn und anschließend Modus ponens den Satz ReadingAvailable. Jede Zeile nennt die Information und die Regel, die sie rechtfertigen.

Diese Regeln erhalten die Wahrheit, sind aber wegen ihrer beschränkten Ausdrucksmöglichkeiten als vollständiges Beweissystem unvollständig. Aus P folgt semantisch der Satz P ∨ Q, doch keine der beiden Regeln führt ∨ ein. Eine Menge korrekter Regeln kann trotzdem gültige Schlussfolgerungen übersehen.

Forme um, ohne die Bedeutung zu ändern

Nützliche Äquivalenzen lassen sich in beide Richtungen anwenden:

• Doppelte Negation: ¬¬P ≡ P.
• Implikation: P ⇒ Q ≡ ¬P ∨ Q.
• Kontraposition: P ⇒ Q ≡ ¬Q ⇒ ¬P.
• Äquivalenz: P ⇔ Q ≡ (P ⇒ Q) ∧ (Q ⇒ P).
• De Morgan: ¬(P ∨ Q) ≡ ¬P ∧ ¬Q und ¬(P ∧ Q) ≡ ¬P ∨ ¬Q.
• Distributivität: P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R), mit dem dualen Gesetz für ∧ über ∨.

Konjunktion und Disjunktion erlauben auch Umgruppierung und Umordnung. Diese Umformungen legen eine nützliche Struktur eines Satzes offen, ohne eine neue Tatsachenannahme hinzuzufügen.

Zerlege bei B₁₁ ⇔ (P₁₂ ∨ P₂₁) und ¬B₁₁ die Äquivalenz und wähle (P₁₂ ∨ P₂₁) ⇒ B₁₁. Kontraposition ergibt ¬B₁₁ ⇒ ¬(P₁₂ ∨ P₂₁). Modus ponens ergibt ¬(P₁₂ ∨ P₂₁); de Morgan ergibt ¬P₁₂ ∧ ¬P₂₁. Und-Elimination beweist dann ¬P₁₂. Der Beweis muss nicht jede mögliche Anordnung in der Höhle aufzählen.

Prüfe einen ungültigen Kurzschluss

Aus P ⇒ Q und Q auf P zu schließen, ist die Bejahung des Konsequens. Aus P ⇒ Q und ¬P auf ¬Q zu schließen, ist die Verneinung des Antezedens. Beide scheitern im Modell P falsch, Q wahr. Ein Serverausfall kann verhindern, dass eine Seite lädt, aber ein Ladefehler kann andere Ursachen haben; auch das Fehlen eines Serverausfalls garantiert keinen Erfolg.

Die Suche nach einem Beweis ist ein Suchproblem. Der Anfangszustand enthält die KB; eine Aktion wendet eine Inferenzregel an und fügt ihre Schlussfolgerung hinzu; der Zielzustand enthält die Anfrage. Die Beweislänge kann als Pfadkosten dienen. Die Auswahl relevanter Sätze verhindert Aufwand für sachfremde Schlussketten. Klassische Logik ist monoton: Das Hinzufügen von Prämissen erhält frühere logische Folgerungen. Default-Regeln mit Ausnahmen brauchen eine andere Behandlung, weil spätere Informationen eine frühere Default-Schlussfolgerung zurücknehmen können.

Resolution beweist eine logische Folgerung, indem sie nach einem Widerspruch sucht. Ihre Eingabe ist die konjunktive Normalform (KNF): eine UND-Verknüpfung von Klauseln, die jeweils eine ODER-Verknüpfung von Literalen sind. Eine Klausel mit einem Literal ist eine Einheitsklausel. Die leere Klausel hat kein Literal, das wahr sein könnte, und steht für Falschheit.

Wandle Sätze in Klauseln um

Eliminiere zuerst ⇔ und ⇒. Ziehe dann Negationen mithilfe der de Morganschen Gesetze und der Eliminierung doppelter Negationen nach innen. Verteile schließlich ∨ über ∧. Eine Äquivalenz kann daher mehrere Klauseln erzeugen.

Bei B₁₁ ⇔ (P₁₂ ∨ P₂₁) ergibt die Hinrichtung ¬B₁₁ ∨ P₁₂ ∨ P₂₁. Die Rückrichtung ergibt ¬(P₁₂ ∨ P₂₁) ∨ B₁₁. Ziehst du die Negation nach innen und verteilst, erhältst du ¬P₁₂ ∨ B₁₁ und ¬P₂₁ ∨ B₁₁. Für die vollständige Äquivalenz werden alle drei Klauseln benötigt.

Resolviere ein komplementäres Paar

Aus P ∨ A und ¬P ∨ B leitet Resolution A ∨ B ab. Welchen Wert P auch hat, mindestens einer der verbleibenden Teile muss gelten. Einheitsresolution verwendet eine Klausel mit einem Literal: P mit ¬P ∨ B ergibt B. Doppelte Literale werden herausfaktorisiert, sodass die Resolution von A ∨ B mit A ∨ ¬B den Satz A ergibt.

Resolviere jeweils genau ein komplementäres Paar. A ∨ B und ¬A ∨ ¬B sind gemeinsam erfüllbar, wenn A wahr und B falsch ist. Das Entfernen beider Paare würde fälschlich die leere Klausel ergeben. Resolution nur über A erzeugt B ∨ ¬B, eine Tautologie, die keine zusätzliche Bedingung darstellt.

Widerlege die negierte Anfrage

Um KB ⊨ α zu beweisen, füge ¬α hinzu, wandle den gesamten Satz in KNF um und leite neue Resolventen ab. Das Erreichen der leeren Klausel beweist, dass kein Gegenmodell existiert.

Füge für die Grubenanfrage ¬P₁₂ den Satz P₁₂ hinzu. Resolviere ihn mit ¬P₁₂ ∨ B₁₁, um B₁₁ zu erhalten. Resolviere das mit dem beobachteten ¬B₁₁, um die leere Klausel zu erreichen. Der Beweis zeigt das Fehlen der Grube, nicht ihr Vorhandensein: Das positive Grubenliteral war eine vorübergehend angenommene negierte Anfrage.

Ein zweites Beispiel verwendet R ⇒ C, (C ∨ I) ⇒ G und R. Die KNF-Klauseln sind ¬R ∨ C, ¬C ∨ G, ¬I ∨ G und R. Füge ¬G hinzu. Die Resolution mit ¬C ∨ G ergibt ¬C, was mit der ersten Klausel ¬R ergibt. Die Resolution von ¬R mit R schließt die Widerlegung ab. Über I wurde kein Fakt benötigt.

Aussagenlogische Resolution ist korrekt und widerlegungsvollständig. Sie terminiert, weil endlich viele Symbole nur endlich viele verschiedene Klauseln erlauben. Entstehen beim vollständigen Bilden des Abschlusses weder eine neue Klausel noch ein Widerspruch, folgt die Anfrage nicht logisch. Resolution muss nicht jeden logisch folgenden Satz direkt ableiten: Aus A allein konstruiert sie nicht A ∨ B.

Durch das Distributivgesetz kann die KNF exponentiell wachsen. Eine Tseitin-Transformation führt Symbole für Teilformeln ein und ergibt eine KNF linearer Größe. Der neue Satz ist genau dann erfüllbar, wenn das Original erfüllbar ist; über dem erweiterten Vokabular muss er zu ihm nicht logisch äquivalent sein. Für SAT-basierte Widerspruchsprüfungen genügt es, die Erfüllbarkeit zu erhalten.

Regeln mit einer positiven Schlussfolgerung erlauben ein einfacheres Inferenzverfahren als allgemeine Resolution. Eine definite Klausel hat genau ein positives Literal; ¬A ∨ ¬B ∨ C wird als A ∧ B ⇒ C geschrieben. Ein Fakt hat einen leeren Rumpf. Eine Horn-Klausel hat höchstens ein positives Literal, darunter fällt auch eine Zielklausel ohne positives Literal wie A ∧ B ⇒ Falsch.

Lass Fakten die Regeln steuern

Vorwärtsverkettung beginnt mit bekannten Fakten. Sind alle Prämissen einer Regel bekannt, füge ihren Kopf hinzu. Fahre fort, bis die Anfrage erscheint oder ein Fixpunkt nichts mehr hinzufügt. Effiziente Implementierungen führen eine Agenda neuer Fakten und zählen pro Regel die noch nicht erfüllten Prämissen.

Nimm PowerOn, FanSpinning und LoadLow als Fakten. Die Regeln sind PowerOn ∧ FanSpinning ⇒ Cooling; Cooling ∧ LoadLow ⇒ TempNormal; PowerOn ⇒ LedLit; LedLit ∧ TempNormal ⇒ SystemOK; FanSpinning ⇒ NoiseHeard. Die Verarbeitung von PowerOn ermöglicht LedLit und erfüllt die Kühlregel teilweise. FanSpinning ermöglicht Cooling und NoiseHeard. Cooling zusammen mit LoadLow ergibt TempNormal, dann ergeben TempNormal und LedLit den Satz SystemOK. NoiseHeard ist eine gültige zusätzliche Schlussfolgerung, obwohl sie für die Anfrage nicht benötigt wurde.

Lass eine Anfrage die Regeln wählen

Rückwärtsverkettung beginnt mit SystemOK. Dessen Regel benötigt LedLit und TempNormal. LedLit wird auf das bekannte PowerOn zurückgeführt. TempNormal benötigt Cooling und LoadLow; Cooling benötigt PowerOn und FanSpinning. Jedes Blatt ist ein Fakt, also ist die Anfrage erfolgreich. Die Geräuschregel wird nie untersucht.

Für KBs aus definiten Klauseln und atomare Anfragen sind beide Verfahren bei geeigneter Suchsteuerung korrekt und vollständig. Aussagenlogische Vorwärtsverkettung kann in einer zur KB-Größe linearen Zeit ablaufen. An ihrem Fixpunkt ergibt sich ein Modell der definiten Klauseln, wenn abgeleitete Symbole auf wahr und alle anderen auf falsch gesetzt werden.

Behandle Zyklen, ohne Antworten zu verlieren

A ⇒ B und B ⇒ A führen bei einem naiven Rückwärtsverfahren zu einer Endlosschleife. Ein Zweig kann anhalten, wenn sein Ziel bereits auf dem aktiven Zielstapel liegt. Erfolgreiche Teilziele können zwischengespeichert werden, aber ein durch eine Schleife verursachter Fehlschlag ist vorübergehend. Bei B ⇒ A, A ⇒ B, C ⇒ A und dem Fakt C kann ein früher Versuch, B zu beweisen, scheitern, während A aktiv ist. Nach dem Beweis von A aus C gelingt ein erneuter Versuch für B. Würde der erste Fehlschlag dauerhaft gespeichert, ginge der Beweis verloren. Tabling verfolgt abhängige Ziele und betrachtet sie erneut, wenn Antworten erscheinen.

Verkettung hängt von der Regelform ab. A ∨ B hat zwei positive Literale und ist daher keine Horn-Klausel. Zusammen mit A ⇒ C und B ⇒ C folgt daraus C, wenn man beide Alternativen betrachtet. Aus der Disjunktion allein wird keine definite Regel ausgelöst. Allgemeine Resolution kann diese Schlussfolgerung beweisen, obwohl einfache Verkettung nicht weiterkommt.

Ein SAT-Löser sucht eine Belegung, die jede Klausel eines KNF-Satzes erfüllt. Ein zurückgegebenes Modell lässt sich direkt überprüfen. Das Ergebnis „unerfüllbar“ schließt alle Belegungen aus. SAT ist NP-vollständig, aber strukturierte Instanzen lassen sich oft viel schneller lösen als durch vollständiges Aufzählen einer Wahrheitstabelle.

Verringere den Suchaufwand mit DPLL

DPLL ist tiefenzuerst ausgeführtes Backtracking mit drei Abkürzungen. Ein wahres Literal erfüllt seine gesamte Klausel, während eine vollständig falsche Klausel den Zweig beendet. Ein reines Symbol kommt in unerfüllten Klauseln nur mit einem Vorzeichen vor und kann daher so belegt werden, dass diese Vorkommen erfüllt sind. Eine Einheitsklausel hat nur noch ein Literal, das wahr sein kann und deshalb auf wahr gesetzt werden muss. Das Wiederholen solcher erzwungenen Entscheidungen ist Einheitspropagation.

Betrachte (A), (¬A ∨ B), (¬B ∨ C ∨ D), (¬C ∨ ¬D), (D ∨ E). E ist rein, setze es also auf wahr. Die Einheitsklausel A erzwingt A wahr, was B wahr erzwingt. Die verbleibende Bedingung C ∨ D und die Klausel ¬C ∨ ¬D verlangen, dass genau eines von C und D wahr ist. Verzweige mit C wahr; Propagation erzwingt D falsch. A, B, C und E wahr mit D falsch erfüllen jede Klausel.

Verzweige bei (A ∨ B), (A ∨ ¬B), (¬A ∨ C), (¬A ∨ ¬C) nach A. A falsch erzwingt sowohl B als auch ¬B; A wahr erzwingt sowohl C als auch ¬C. Beide Zweige führen zu einem Konflikt, also ist der gesamte Satz unerfüllbar.

Lerne aus Konflikten

Konfliktgesteuertes Klausellernen (CDCL) erweitert diese Suche. Eine gelernte Klausel blockiert eine Kombination, die für einen Konflikt verantwortlich ist. Backjumping überspringt irrelevante Entscheidungen; die Aktivität von Variablen steuert die Verzweigung; Neustarts ändern den Suchweg; überwachte Literale beschleunigen die Propagation. Gelernte Klauseln sind durch die Formel begründet und erhalten somit ihre möglichen Lösungen.

Suche durch Veränderung einer vollständigen Belegung

WalkSAT beginnt mit einer zufälligen vollständigen Belegung. Es wählt eine unerfüllte Klausel und kehrt den Wert einer Variablen darin um, manchmal zufällig und manchmal so, dass die meisten Klauseln erfüllt bleiben. Zufällige Schritte helfen, lokalen Fallen zu entkommen. Sind zu Beginn im früheren Beispiel alle fünf Symbole falsch, sind (A) und (D ∨ E) falsch. Die Umkehrung von A erfüllt (A), macht aber (¬A ∨ B) falsch. Ein Schritt kann eine Klausel reparieren und zugleich eine andere verletzen.

Gib zur Prüfung einer logischen Folgerung KB ∧ ¬α ein. Unerfüllbarkeit beweist α; ein Modell ist ein Gegenbeispiel. Ein Zeitlimit bei WalkSAT lässt beide Möglichkeiten offen. In großen zufälligen 3-KNF-Formeln liegt der geschätzte Übergang beim Verhältnis von Klauseln zu Variablen nahe 4,26; schwierige Instanzen liegen häufig in seiner Nähe. Dies ist ein Muster für eine Gesamtheit von Instanzen und kein Schwellenwert, der über eine einzelne Formel entscheidet. Auch Klauselstruktur und Löserstrategie beeinflussen die Schwierigkeit.

Die Prädikatenlogik erster Stufe beschreibt Objekte und ihre Beziehungen. Statt jedem Feld ein eigenes, unverbundenes Symbol zu geben, kann sie eine Regel für alle Felder ausdrücken: ∀s (Breezy(s) ⇔ ∃r (Adjacent(r, s) ∧ Pit(r))). Quantoren machen Allgemeinheit zu einem Bestandteil der Sprache.

Trenne Objekte von Aussagen

Eine Konstante benennt ein Objekt, etwa Ada. Eine Variable wie x durchläuft Objekte. Eine Funktion bildet Objekte auf ein Objekt ab: MotherOf(Ada) ist ein Term, der eine Person bezeichnet. Ein Prädikat bildet eine Aussage: Owns(Ada, Atlas) ist wahr oder falsch. Ein Term kann eine Konstante, eine Variable oder eine auf Terme angewendete Funktion sein.

Book(x) ist ein Satz und kein Objekt, sodass Owns(Ada, Book(x)) einen Ausdruck der falschen Art an eine Argumentstelle setzt. Gleichheit vergleicht, worauf sich Terme beziehen: MotherOf(Ada) = Clara besagt, dass beide Terme dasselbe Objekt bezeichnen.

Werte einen Satz in einem Modell aus

Ein prädikatenlogisches Modell liefert einen nicht leeren Individuenbereich und eine Interpretation. Konstanten bezeichnen Objekte des Individuenbereichs, Prädikate bezeichnen Relationen, und Funktionen liefern für jedes geeignete Tupel von Objekten des Individuenbereichs Ausgaben. Ein allquantifizierter Satz muss für jeden möglichen Wert seiner Variablen gelten; ein existenzieller Satz benötigt mindestens einen Zeugen.

Der Individuenbereich sei {a, b, k}; Ada bezeichnet a, Ben bezeichnet b und Atlas bezeichnet k. Person enthält a und b, Book enthält k und Owns enthält nur (a, k). Owns(Ada, Atlas) ist wahr. ∃x (Book(x) ∧ Owns(Ben, x)) ist falsch, weil Ben kein Objekt besitzt. ∀x (Person(x) ⇒ ∃y (Book(y) ∧ Owns(x, y))) ist falsch, weil Ben ein Gegenbeispiel ist. Dennoch hat jedes Buch einen Besitzer: ∀x (Book(x) ⇒ ∃y Owns(y, x)) gilt.

Mache Modellierungsannahmen ausdrücklich

Die Prädikatenlogik erster Stufe mit Standardsemantik schreibt diese Datenbankannahmen nicht vor. Book(Atlas), Book(Beowulf), Owns(Ada, Atlas) und Owns(Ada, Beowulf) lassen offen, ob die beiden Namen dasselbe Buch bezeichnen und ob Ada weitere Bücher besitzt. Unter Datenbanksemantik beschreiben sie genau zwei Bücher in Adas Besitz.

Um genau diese Aussage unter Standardsemantik zu erhalten, behalte die vier Fakten bei und füge ¬(Atlas = Beowulf) und ∀x ((Book(x) ∧ Owns(Ada, x)) ⇒ (x = Atlas ∨ x = Beowulf)) hinzu. Die Ungleichheit stellt sicher, dass es zwei verschiedene Bücher sind; die universelle Einschränkung schließt weitere Bücher in Adas Besitz aus.

Prädikatenlogische Modelle können beliebig große Individuenbereiche haben, sodass das endliche Aufzählungsverfahren für aussagenlogische Modelle hier kein allgemeines Entscheidungsverfahren liefert. Beweisverfahren arbeiten stattdessen mit der Struktur der Sätze. Eine freie Variable braucht zur Auswertung eine Belegung; binde Variablen, wenn du eine geschlossene Aussage für die KB formulierst.

Übersetzen beginnt mit der Entscheidung, was der Satz über jedes Objekt aussagt. Quantorengeltungsbereich, Implikationsrichtung und Gleichheit bestimmen die Bedeutung; Prädikatsnamen allein legen sie nicht fest. Klammern machen den beabsichtigten Geltungsbereich sichtbar.

Verwende den richtigen Junktor mit einem Quantor

„Jede Katze ist ein Säugetier“ wird zu ∀x (Cat(x) ⇒ Mammal(x)). Ein Objekt außerhalb der Kategorie erfüllt die Implikation, ohne eine Katze zu sein. ∀x (Cat(x) ∧ Mammal(x)) zu schreiben, macht fälschlich alles zu einer Katze.

„Eine Katze ist schwarz“ wird zu ∃x (Cat(x) ∧ Black(x)). Der Zeuge muss beide Eigenschaften erfüllen. Bei ∃x (Cat(x) ⇒ Black(x)) ist jedes Objekt, das keine Katze ist, bereits ein Zeuge, selbst in einer Welt ohne schwarze Katzen. Universelle Kategorieregeln verwenden gewöhnlich Implikation; existenzielle Kategorieaussagen gewöhnlich Konjunktion.

Prüfe, wer von wem abhängen kann

∀x ∃y Loves(x, y) erlaubt für jedes x eine andere geliebte Person. ∃y ∀x Loves(x, y) verlangt eine Person, die von allen geliebt wird. In einer Welt mit zwei Personen, in der jede nur die andere liebt, gilt der erste Satz und der zweite nicht. Das Vertauschen verschiedenartiger Quantoren kann eine Aussage ändern; das Vertauschen zweier benachbarter Allquantoren oder zweier benachbarter Existenzquantoren erhält sie.

Negation vertauscht Quantoren: ¬∀x P(x) ≡ ∃x ¬P(x) und ¬∃x P(x) ≡ ∀x ¬P(x). Daher bedeutet „Nicht jeder Studierende hat bestanden“ dasselbe wie ∃x (Student(x) ∧ ¬Passed(x)). Dies verlangt einen Studierenden, der nicht bestanden hat; es behauptet nicht, dass alle Studierenden nicht bestanden haben.

Drücke Richtung und Anzahl aus

„Nur Mitglieder leihen aus“ bedeutet ∀x (Borrows(x) ⇒ Member(x)). Ausleihen reicht aus, um Mitgliedschaft festzustellen, während Mitgliedschaft allein nichts über das Ausleihen aussagt. „Kein Reptil ist ein Säugetier“ bedeutet ∀x (Reptile(x) ⇒ ¬Mammal(x)).

Um mindestens zwei Bücher in Adas Besitz auszudrücken, schreibe ∃x ∃y (Book(x) ∧ Book(y) ∧ Owns(Ada, x) ∧ Owns(Ada, y) ∧ ¬(x = y)). Die Ungleichheit ist wichtig: Zwei Variablennamen können dasselbe Objekt bezeichnen. Genau eines verwendet einen Zeugen plus Eindeutigkeit: ∃x (Book(x) ∧ Owns(Ada, x) ∧ ∀y ((Book(y) ∧ Owns(Ada, y)) ⇒ y = x)).

Gib Definitionen in beide Richtungen

Eine Definition von Geschwistern kann lauten: ∀x ∀y (Sibling(x, y) ⇔ (¬(x = y) ∧ ∃p (Parent(p, x) ∧ Parent(p, y)))). Die Hinrichtung schränkt ein, wer Geschwister sein kann; die Rückrichtung ermöglicht es, anhand von Fakten über einen gemeinsamen Elternteil Geschwisterschaft festzustellen. Eine einseitige Implikation liefert nur die Hälfte dieser Bedeutung.

In einer Agentendomäne führen diagnostische Regeln von Beobachtungen zu möglichen Ursachen, während kausale Regeln von Ursachen zu Wirkungen führen. „Jedes Feld mit Lufthauch hat eine benachbarte Grube“ ist diagnostisch. „Jede Grube verursacht auf jedem benachbarten Feld einen Lufthauch“ ist kausal. Zusammen stützen sie die vollständige Lufthauchäquivalenz. Schließe eine Übersetzung ab, indem du die Bindung jeder Variablen prüfst und eine kleine Welt testest, in der die deutsche Aussage falsch sein sollte.

Eine nützliche Wissensbasis zu erstellen ist eine Modellierungsaufgabe. Formale Notation hilft erst, nachdem die relevanten Fragen, Objekte und Beziehungen gewählt wurden. Wissensengineering macht aus diesen Entscheidungen Axiome, die sich anhand beabsichtigter Beispiele prüfen lassen.

Richte den Aufbau an den Fragen aus

Eine praktische Abfolge besteht darin, die Aufgabe zu bestimmen, relevantes Wissen zusammenzutragen, ein Vokabular zu wählen, allgemeine Axiome zu formulieren, Instanzfakten hinzuzufügen, Anfragen zu stellen und Fehler in den Ergebnissen zu beheben. Beginne mit konkreten Fragen wie „Kann sich diese Person für diesen Kurs einschreiben?“ Diese Frage bestimmt, was die Repräsentation ermöglichen muss.

Verwende für die Einschreibung Student(s), Course(c), Prereq(p, c), Passed(s, c) und CanEnroll(s, c). Prereq(p, c) bedeutet, dass p vor c bestanden werden muss; das Vertauschen der Argumente würde die Abhängigkeit umkehren. Eine Regel lautet ∀s ∀c ((Student(s) ∧ Course(c) ∧ ∀p (Prereq(p, c) ⇒ Passed(s, p))) ⇒ CanEnroll(s, c)). Sie verlangt jede Voraussetzung, nicht nur eine.

Trenne wiederverwendbare Regeln von einer Instanz

Angenommen, die Fakten sind Student(Mia), Course(AI), Prereq(Logic, AI), Prereq(Programming, AI), Passed(Mia, Logic) und Passed(Mia, Programming). Die allgemeine Regel lässt sich für andere Studierende und Kurse wiederverwenden, während diese Instanzfakten einen Fall beschreiben.

Unter Standardsemantik der Prädikatenlogik erster Stufe lassen diese Fakten zusätzliche Voraussetzungen für AI offen. Ein vereinbares Modell könnte eine nicht bestandene dritte Voraussetzung enthalten, sodass CanEnroll(Mia, AI) noch nicht logisch folgt. Füge ∀p (Prereq(p, AI) ⇔ (p = Logic ∨ p = Programming)) hinzu, um die Liste zu vervollständigen. Nun ist jede Voraussetzung einer der beiden bestandenen Kurse, und die Einschreibungsregel gilt. Eine Datenbank mit geschlossener Welt kann dieselbe Antwort erhalten, indem sie fehlende Fakten über Voraussetzungen als falsch behandelt.

Wähle, was zu einem Objekt wird

Eine Ontologie besteht aus dem Vokabular und seinen strukturellen Annahmen. Red(x) behandelt Rot als Eigenschaft. Color(x, Red) macht Red zu einem Objekt, sodass ∃c (Color(x, c) ∧ Color(y, c)) eine gemeinsame Farbe ausdrücken kann. Dieser Schritt ist Reifikation: Er erlaubt es der Sprache, über eine Eigenschaft oder Kategorie als etwas Eigenständiges zu sprechen.

ASK kann fragen, ob CanEnroll(Mia, AI) folgt. ASKVARS kann Bindungen für CanEnroll(x, AI) anfordern und eine Substitution wie {x/Mia} zurückgeben. Dieselbe KB unterstützt sowohl Fragen nach Wahrheitswerten als auch Anfragen nach passenden Objekten.

Prüfe die Bedeutung, nicht nur die Syntax

Ein fehlendes Axiom kann eine gewünschte logische Folgerung verhindern; ein fehlerhaftes Axiom kann eine unerwünschte stützen. Teste positive Beispiele, negative Beispiele und Grenzfälle. Die Regel ∀c (Course(c) ⇒ ∃t Teaches(t, c)) ist zu stark, wenn manche Kurse noch keine Lehrkraft haben. Die Regel ∀p ∀c (Prereq(p, c) ⇒ Passed(Mia, p)) ist zu stark, weil sie Mia jede Voraussetzung jedes Kurses zuschreibt.

Prädikatsnamen sind für das Inferenzsystem Bezeichnungen. Eine Relation Prereq zu nennen, legt für sich genommen keine Einschreibungsregel fest. Die Regeln müssen Voraussetzungen, bestandene Kurse und Einschreibungsberechtigung in der beabsichtigten Richtung verbinden.

Prädikatenlogische Inferenz arbeitet mit Mustern, die Variablen enthalten. Substitution ersetzt Variablen durch Terme; Unifikation findet Ersetzungen, die zwei Ausdrücke identisch machen. Zusammen ermöglichen sie, eine allgemeine Regel für viele konkrete Fakten zu verwenden, ohne zuerst jede mögliche Instanz zu erzeugen.

Instanziiere quantifizierte Sätze sorgfältig

Universelle Instanziierung ersetzt eine universell gebundene Variable durch einen beliebigen Grundterm. Leite aus ∀x (Cat(x) ⇒ Mammal(x)) den Satz Cat(Tom) ⇒ Mammal(Tom) oder die entsprechende Instanz mit MotherOf(Tom) ab. Ein Grundterm enthält keine Variable.

Existenzielle Instanziierung führt einen neuen Zeugennamen ein. Führe aus ∃x (Crown(x) ∧ OnHead(x, John)) eine neue Konstante C₁ ein und füge Crown(C₁) und OnHead(C₁, John) hinzu. Stattdessen Ben als Zeugen zu benennen, würde ein nicht näher bestimmtes Objekt fälschlich mit einem vorhandenen gleichsetzen. Die erweiterte KB erhält die Erfüllbarkeit, nicht aber die Äquivalenz im vergrößerten Vokabular.

Propositionierung erzeugt Grundinstanzen und nutzt dann aussagenlogisches Schließen. Funktionssymbole können unendlich viele Terme erzeugen: Ada, MotherOf(Ada), MotherOf(MotherOf(Ada)) und so weiter. Logisch folgende prädikatenlogische Anfragen haben endliche Beweise, aber ein allgemeiner Beweiser kann endlos laufen, wenn die Anfrage nicht logisch folgt. Das ist Semientscheidbarkeit.

Finde eine konsistente Substitution

Um Knows(Ana, x) mit Knows(y, Bo) zu unifizieren, gleiche zuerst Prädikat und Stelligkeit ab. Die ersten Argumente verlangen y = Ana; die zweiten verlangen x = Bo. Die Substitution {y/Ana, x/Bo} macht beide Ausdrücke zu Knows(Ana, Bo).

Knows(Ana, x) und Knows(y, MotherOf(y)) ergeben stattdessen {y/Ana, x/MotherOf(Ana)}. Eine Bindung muss in die anderen Terme übernommen werden. Kommt dieselbe Variable x in beiden Ausdrücken Knows(Ana, x) und Knows(x, Bo) vor, müsste sie sowohl Ana als auch Bo werden, sodass die syntaktische Unifikation scheitert.

Variablen in getrennt quantifizierten Sätzen sind unabhängig. Variablenumbenennung benennt sie um, bevor Sätze kombiniert werden. Benennt man im letzten Paar das zweite x in z um, ist {z/Ana, x/Bo} möglich. Dies erhält die beabsichtigte Unabhängigkeit der lokalen Variablen zweier Regeln.

Ein allgemeinster Unifikator (MGU) legt keine unnötigen Bindungen fest. Knows(Ana, x) und Knows(y, z) lassen sich mit {y/Ana, x/z} unifizieren; auch z auf Ana zu setzen würde das Ergebnis unnötig spezialisieren. Die Vorkommensprüfung verwirft x = MotherOf(x), da ein endlicher Term sich nicht selbst enthalten kann. Die gewöhnliche Unifikation in Prolog kann zyklische Terme zulassen, sodass ihr Verhalten sorgfältig zu beachten ist, wenn Prädikatenlogik erster Stufe mit endlichen Termen gemeint ist.

Wende die abgeglichene Regel an

Der verallgemeinerte Modus ponens gleicht jede Prämisse unter einer konsistenten Substitution ab. Owns(Ada, Atlas) und Book(Atlas) passen mit {x/Ada, y/Atlas} zu Owns(x, y) ∧ Book(y) ⇒ Reader(x), was Reader(Ada) ergibt. Eine Prämisse mit y = Atlas und eine andere mit y = Beowulf abzugleichen würde das Auslösen der Regel nicht rechtfertigen: Gemeinsame Variablen erzwingen dieselben Objekte.

Eine definite Klausel der Prädikatenlogik erster Stufe hat atomare Prämissen und eine atomare Schlussfolgerung; ihre Variablen gelten als allquantifiziert. Vorwärts- und Rückwärtsverkettung nutzen Unifikation, um diese Regeln auf benannte Objekte anzuwenden. Datalog behält diese Regelform bei und schließt Funktionssymbole aus. Dadurch ergibt sich im üblichen Fall einer endlichen Datenbank ein endlicher Raum möglicher Grundfakten.

Leite erreichbare Orte ab

Nimm Link(A, B), Link(B, C) und Link(C, D). Verwende Link(x, y) ⇒ Reach(x, y) und Link(x, y) ∧ Reach(y, z) ⇒ Reach(x, z). In synchronen Runden liest jede Regel die Fakten, die vor der jeweiligen Runde verfügbar waren.

Runde 1 leitet Reach(A, B), Reach(B, C) und Reach(C, D) ab. Runde 2 fügt Reach(A, C) und Reach(B, D) hinzu. Runde 3 fügt Reach(A, D) hinzu. Runde 4 fügt nichts hinzu. Am Fixpunkt gibt es sechs Reach-Fakten. Eine Implementierung, die neue Fakten sofort wiederverwendet, kann sie in anderer Reihenfolge finden, erreicht aber denselben Abschluss.

Bei n Konstanten und Prädikaten mit einer Stelligkeit von höchstens k sind nur endlich viele Tupel möglich; eine obere Schranke ist p · nᵏ für p Prädikate. Dagegen erzeugen NatNum(0) und NatNum(n) ⇒ NatNum(S(n)) endlos immer tiefere Terme. Funktionssymbole heben die Garantie eines endlichen Bereichs auf.

Das Abgleichen einer Regel mit mehreren Prämissen ist ein Constraint-Problem. Eine selektive Prämisse kann die danach betrachteten Substitutionen stark reduzieren. Inkrementelle Vorwärtsverkettung konzentriert sich auf Regeln, die von neu hinzugefügten Fakten betroffen sind. Rete-Netze behalten teilweise Übereinstimmungen über Aktualisierungen hinweg und vermeiden so wiederholte Arbeit in Produktionsregelsystemen.

Arbeite mit Bindungen rückwärts

Um Reach(A, D) zu beweisen, versuche die Regel für eine direkte Verbindung, die das fehlende Link(A, D) benötigt. Die rekursive Regel benötigt stattdessen Link(A, y) und Reach(y, D). Das Erste bindet y an B. Setzt man über B und C fort, erreicht man das bekannte Link(C, D). Die Anfrage Reach(A, w) hat drei Antworten: w = B, C oder D.

Prolog schreibt Regeln mit dem Kopf zuerst und verwendet großgeschriebene Variablen und kleingeschriebene Konstanten:

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

Es versucht Klauseln von oben nach unten und Prämissen von links nach rechts mittels tiefenzuerst ausgeführter Rückwärtsverkettung. Arithmetik kann N is M + 1 verwenden. Negation durch Fehlschlag, geschrieben \+ p, ist erfolgreich, wenn der Versuch, p zu beweisen, nach endlicher Zeit scheitert. Es ist eine operative Prüfung auf Fehlschlag, kein allgemeiner Beweis klassischer Negation.

Verhindere, dass Rekursion die Suche festhält

Steht reach(X, Y) im rekursiven Rumpf zuerst, kann es sofort dasselbe ungelöste Ziel erneut aufrufen. Basisklauseln zuerst und Rekursion, die eine Verbindung abarbeitet, helfen, aber Zyklen können erfolglose Suchen weiterhin festhalten. Tabling speichert Antworten auf Teilziele und verwaltet wiederholte Abhängigkeiten. Vorwärtsverkettung ist für endliches Datalog vollständig; naive tiefenzuerst ausgeführte Rückwärtssuche braucht eine solche Steuerung, um erreichbare Antworten hinter unendlichen Zweigen nicht zu übersehen.

Prädikatenlogische Resolution erweitert das Schließen mit Klauseln um Unifikation. Sie kann Schlussfolgerungen über unbenannte Objekte beweisen, weil Skolem-Terme die Abhängigkeiten existenzieller Zeugen erhalten. Beginne wie bei der aussagenlogischen Widerlegung mit der KB und der Negation der Anfrage.

Bereite prädikatenlogische Klauseln vor

Eliminiere ⇔ und ⇒, ziehe Negationen nach innen, benenne gebundene Variablen um, skolemisiere existenzielle Variablen, lasse Allquantoren weg und verteile dann ∨ über ∧. Die Negation zuerst nach innen zu ziehen ist wichtig, weil aus ¬∀x P(x) der Satz ∃x ¬P(x) wird und sich damit die Art des benötigten Zeugen ändert.

Für „Jeder Kurs hat eine Lehrkraft“, ∀c (Course(c) ⇒ ∃t Teaches(t, c)), kann die existenziell quantifizierte Lehrkraft von c abhängen. Führe eine neue Funktion T(c) ein, um ¬Course(c) ∨ Teaches(T(c), c) zu erhalten. Eine einzelne Konstante würde eine gemeinsame Lehrkraft vorgeben, die der ursprüngliche Satz nicht verlangt. Für ∃t ∀c (Course(c) ⇒ Teaches(t, c)) ist eine neue Konstante angemessen, weil der Zeuge vor dem Allquantor steht.

„Nicht jeder Vogel fliegt“ wird zu ∃x (Bird(x) ∧ ¬Flies(x)), dann zu Bird(B₁) und ¬Flies(B₁). Beide Klauseln verwenden denselben neuen Zeugen. Skolemisierung erhält die Erfüllbarkeit; sie ist keine gewöhnliche Äquivalenz über dem erweiterten Vokabular.

Wende einen Unifikator auf die gesamte Resolvente an

Benenne die Variablen der beiden Klauseln getrennt um. Finde komplementäre Literale, die sich unifizieren lassen, entferne sie und wende ihren MGU auf jedes verbleibende Literal an. Faktorisierung führt außerdem unifizierbare Literale innerhalb einer Klausel zusammen. Resolution mit Faktorisierung ist für prädikatenlogische Klauseln widerlegungsvollständig.

Nimm ¬Course(c) ∨ Teaches(T(c), c), ¬Teaches(u, v) ∨ Staff(u) und Course(Logic). Die Anfrage lautet ∃w Staff(w); ihre Negation ergibt ¬Staff(w), wobei w allquantifiziert ist. Resolviere den Kursfakt mit der ersten Klausel, um Teaches(T(Logic), Logic) zu erhalten. Die Resolution mit der zweiten unter {u/T(Logic), v/Logic} ergibt Staff(T(Logic)). Die Resolution mit ¬Staff(w) unter {w/T(Logic)} führt zur leeren Klausel. Es existiert ein Mitglied des Personals, obwohl die KB dieser Person nie einen gewöhnlichen Namen gibt.

Steuere die Klauselsuche

Einheitspräferenz wählt kurze Klauseln zuerst. Die Stützmengenstrategie verlangt eine Elternklausel aus der negierten Anfrage oder ihren Nachfolgern und erhält die Vollständigkeit, wenn die übrige KB erfüllbar ist. Eingaberesolution verlangt in jedem Schritt eine ursprüngliche Elternklausel und ist für Horn-KBs vollständig. Subsumption entfernt eine schwächere Klausel, die bereits durch eine stärkere allgemeine Klausel abgedeckt ist, etwa P(Ana) ∨ Q(Bo), wenn P(x) bekannt ist.

Gleichheit braucht eine eigene Behandlung: Gleichheitsaxiome, Umschreiben anhand von Gleichungen durch Demodulation oder Inferenzen wie Paramodulation. Rein syntaktische Resolution allein erfasst nicht jede Bedeutung von Gleichheit. Eine faire vollständige Suche findet für jede unerfüllbare prädikatenlogische Klauselmenge einen Widerspruch, kann aber andernfalls endlos laufen. Zu den resolutionsbasierten Beweisern gehören Vampire und E; EQP bewies 1996 die Robbins-Vermutung.

Eine Ontologie ordnet die Kategorien, Objekte, Relationen und Annahmen eines Fachgebiets. Eine obere Ontologie liefert allgemeine Begriffe wie Objekte, Ereignisse und Zeit; eine Fachontologie liefert die für ein bestimmtes Gebiet nützlichen Unterscheidungen. Klinische und biologische Ontologien zeigen, warum ein nützliches gemeinsames Vokabular häufig einer bestimmten Fachgemeinschaft dient.

Halte Zugehörigkeit und Unterklassenbeziehung getrennt

Eine Kategorie kann als Prädikat Laptop(x) oder als Objekt Laptops auftreten. Die Zugehörigkeit x ∈ Laptops besagt, dass ein Individuum dazu gehört. Laptops ⊂ Computers besagt, dass jeder Laptop ein Computer ist. Eine Taxonomie ordnet solche Unterklassenbeziehungen in einer Hierarchie. Wenn jeder Computer einen Prozessor hat, erben Laptops diese Eigenschaft.

Die Unterklassenbeziehung ist transitiv: Aus Penguins ⊂ Birds und Birds ⊂ Animals folgt Penguins ⊂ Animals. Zugehörigkeit ist nicht transitiv. Aus Pingu ∈ Penguins und Penguins ∈ Species folgt nicht, dass Pingu eine Art ist. Eine Aussage betrifft einen einzelnen Vogel; die andere betrifft eine Kategorie, die als Objekt behandelt wird.

Kategorien sind disjunkt, wenn sie keine Mitglieder gemeinsam haben. Eine erschöpfende Zerlegung deckt jedes Mitglied der übergeordneten Kategorie ab. Eine Partition erfüllt beides: Negative ganze Zahlen, null und positive ganze Zahlen partitionieren die ganzen Zahlen. Erschöpfung erlaubt Überschneidungen, sofern nicht auch Disjunktheit angegeben ist.

Stelle Teile, Ereignisse und geerbte Werte dar

PartOf beschreibt Zusammensetzung, nicht Kategoriezugehörigkeit. PartOf ist transitiv: Eine Speiche, die zu einem Rad gehört, das zu einem Fahrrad gehört, ist Teil des Fahrrads. Ein Fahrrad ist dadurch keine Art von Rad. Auch Ereignisse können Objekte sein: Happens(e, t), Initiates(e, f, t) und HoldsAt(f, t) verbinden Ereignisse mit veränderlichen Fluents. Das Einschalten einer Lampe setzt einen Fluent in Gang, der fortbesteht, bis ein Ereignis ihn beendet.

Ein semantisches Netz stellt Objekte und Kategorien als Knoten mit beschrifteten Relationen dar. In einem Netz mit Defaults kann „Vögel fliegen normalerweise“ einen Wert liefern, den gewöhnliche Vögel erben, während eine spezifischere Kategorie der Pinguine ihn überschreibt. Das unterscheidet sich von der ausnahmslosen klassischen Behauptung ∀x (Bird(x) ⇒ Flies(x)), die auch für Pinguine gelten würde.

Wähle die Sprache zum Schlussfolgern

Beschreibungslogiken unterstützen Subsumption, Klassifikation und Konsistenzprüfungen. Eine Definition kann eine Person mit mindestens drei Kindern einer passenden Kategorie zuordnen. Diese Logiken bilden die Grundlage der beschreibungslogischen Sprachen von OWL.

Default-Schließen ist nichtmonoton: Erfährt man, dass ein Vogel ein Pinguin ist, kann dies die Default-Annahme zurücknehmen, dass er fliegt. Zirkumskription minimiert anormale Fälle in Regeln wie Bird(x) ∧ ¬Abnormal(x) ⇒ Flies(x). Default-Logik erlaubt Schlussfolgerungen, solange sie mit dem Wissen vereinbar bleiben. Wahrheitserhaltungssysteme halten die Grundlagen von Schlussfolgerungen fest, sodass von einer zurückgenommenen Überzeugung abhängige Schlussfolgerungen entfernt werden können.

Ein Wissensgraph speichert Entitäten und ihre Beziehungen als gerichteten Graphen. Eine einfache Kante wird zu einem Tripel: Subjekt, Prädikat, Objekt. Beispielsweise entspricht (Ada, worksAt, Lab) dem Satz WorksAt(Ada, Lab); (Ada, type, Researcher) drückt die Zugehörigkeit zu einer Kategorie aus. Ein Schema gibt diesen Bezeichnungen eine gemeinsame Bedeutung und ermöglicht weitere Schlussfolgerungen.

Unterscheide die Webstandards

RDF stellt Graphen als Tripel dar. Subjekte sind IRIs oder leere Knoten, Prädikate sind IRIs und Objekte können auch Literalwerte sein. IRIs identifizieren Ressourcen über Datensätze hinweg; ein leerer Knoten stellt eine Ressource ohne globalen Bezeichner dar. RDFS ergänzt Klassen, Unterklassenbeziehungen sowie Definitions- und Wertebereiche von Eigenschaften. OWL bietet ausdrucksstärkere Ontologiedefinitionen. SPARQL gleicht Graphmuster ab, um Variablenbindungen zurückzugeben. Property-Graphen bieten ein weiteres Modell mit Schlüssel-Wert-Eigenschaften an Knoten und Kanten; Cypher und GQL sind Abfragesprachen für diese Familie.

Wenn Ada als Researcher eingeordnet ist und Researcher eine Unterklasse von Scientist ist, leitet eine Unterklassenregel ab, dass Ada ein Scientist ist. Dies ist prädikatenlogische Vorwärtsverkettung über Member(x, c) ∧ Subset(c, d) ⇒ Member(x, d). Eine Graphabfrage-Engine braucht die entsprechende Unterstützung für logische Folgerung oder materialisierte Schlussfolgerungen, um diesen abgeleiteten Fakt bereitzustellen.

Gleiche eine Anfrage ab und bewahre Details

Wenn ex: als IRI-Präfix deklariert ist, kann eine Anfrage lauten:

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

Dasselbe ?p muss beide Muster erfüllen. Es handelt sich um eine Verknüpfung, nicht um zwei unabhängige Suchen. Ergebnisse sind Bindungen wie ?p = ex:Ada, ähnlich den Substitutionen in logischen Anfragen.

Eine binäre Kante kann für sich genommen nicht jede Rolle in einem datierten Ereignis ausdrücken. Erstelle für eine Auszeichnung einen Ereignis- oder Aussageknoten und verbinde ihn mit der ausgezeichneten Person, dem Preis und dem Jahr. So bleiben die Angaben zu einer Auszeichnung zusammen, und das Datum wird nicht versehentlich jeder Auszeichnung dieser Art zugeordnet. Wikidata unterstützt für solche Details Aussagequalifikatoren.

Unterscheide fehlende, abgeleitete und vorhergesagte Verbindungen

RDF und OWL verwenden eine Lesart nach der Offene-Welt-Annahme: Eine fehlende Ehepartnerkante lässt die Beziehung unbekannt. Anwendungen mit geschlossener Welt treffen bei fehlenden Fakten eine andere Entscheidung. Ein leeres Anfrageergebnis meldet, dass unter den Einstellungen dieser Anfrage keine Übereinstimmung vorliegt; es belegt für sich genommen keinen allgemeinen negativen Fakt.

Wikidata, DBpedia, Googles Knowledge Graph und interne Organisationsgraphen unterstützen Faktenanfragen, Datensatzverknüpfung, Empfehlungen und den Abruf für generative Systeme. Ihre Fakten können unvollständig oder veraltet sein. Entitätsauflösung identifiziert Datensätze, die sich auf dasselbe beziehen, auch wenn ihre Bezeichner verschieden sind.

Einbettungen weisen Entitäten und Relationen Vektoren zu. In TransE wird die Summe aus dem Vektor des Anfangsknotens und dem Relationsvektor darauf trainiert, nahe am Vektor des Endknotens zu liegen. Eine hohe Bewertung legt eine fehlende Verbindung nahe; sie ist eine statistische Vorhersage. Logische Inferenz leitet eine Konsequenz aus angegebenen Fakten und Regeln ab. Halte diesen Unterschied sichtbar, wenn du entscheidest, ob eine neue Kante zu den überprüften Fakten gehört.

Klassisches Planen sucht Aktionen, die von einem bekannten Anfangszustand zu einem Ziel führen. Das Modell ist vollständig beobachtbar, deterministisch und diskret und enthält einen einzelnen Agenten; die Welt verändert sich durch die modellierten Aktionen. Eine faktorisierte Repräsentation beschreibt jeden Zustand durch Fluents, sodass ein Planer darüber nachdenken kann, was jede Aktion verändert.

Schreibe den Zustand und die Aktionsschemata auf

Im grundlegenden STRIPS-artigen Teil von PDDL listet ein Zustand wahre atomare Grundfluents auf. Nicht aufgeführte Fluents sind unter der Geschlossene-Welt-Annahme falsch. Die wiederverwendbare Domäne deklariert Prädikate und Aktionsschemata; das Problem deklariert Objekte, den Anfangszustand und ein Ziel. PDDL wurde für den Planungswettbewerb 1998 eingeführt und baut auf STRIPS auf.

Ein Aktionsschema hat Parameter, eine Vorbedingung und Effekte. Go(r, from, to) benötigt At(r, from) und Connected(from, to); es fügt At(r, to) hinzu und löscht At(r, from). Pick(r, p, l) benötigt At(r, l), In(p, l) und HandEmpty(r); es fügt Holding(r, p) hinzu und löscht In(p, l) und HandEmpty(r). Drop benötigt den Ort und den Besitz des Pakets; es fügt den Ort des Pakets und eine leere Hand hinzu und löscht den Besitz.

Eine Grundaktion ist nur anwendbar, wenn ihre Vorbedingungen gelten. Ihre Aktualisierung lautet RESULT(s, a) = (s − DEL(a)) ∪ ADD(a). Andere Fluents bleiben bestehen, darunter statische Connected-Fakten. Dieses implizite Fortbestehen behandelt das Rahmenproblem ohne ein separates Axiom für jeden unveränderten Fluent.

Verfolge eine Lieferung in vier Aktionen

Anfangs ist R bei Dock, Box bei Shelf und die Hand von R ist leer. Connected-Verbindungen verknüpfen Dock mit Shelf und Shelf mit Packing in beide Richtungen. Das Ziel ist In(Box, Packing).

1. Go(R, Dock, Shelf) ändert den Ort von R und erhält die Fakten über die Kiste und die Hand.
2. Pick(R, Box, Shelf) entfernt die Kiste vom Regal und bewirkt, dass R sie hält.
3. Go(R, Shelf, Packing) bewegt R und erhält dabei Holding(R, Box).
4. Drop(R, Box, Packing) legt die Kiste bei Packing ab und macht die Hand frei.

Das Ziel lässt den endgültigen Ort des Roboters offen, soweit die Aktionen ihn nicht festlegen. Ziele beschreiben im Allgemeinen viele akzeptable Zustände, keinen einzelnen vollständigen Zustand.

Lies und prüfe ein 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))))

Wird ein Löscheffekt ausgelassen, kann ein Roboter an zwei Orten oder ein Paket zugleich in der Hand und auf einem Regal sein. Steht eine erforderliche Bedingung nur in einem Effekt, erzeugt die Aktion sie, statt sie zu prüfen.

In der Klötzchenwelt benötigt das Bewegen eines freien Klötzchens b von x auf ein freies Klötzchen y die Bedingungen On(b, x), Clear(b), Clear(y), Block(b), Block(y) und ¬(b = y). Es fügt On(b, y) und Clear(x) hinzu und löscht On(b, x) und Clear(y). Die Prüfungen auf Verschiedenheit und Klötzchen verhindern, dass ein Klötzchen auf sich selbst gestapelt oder der Tisch wie ein einzelnes Klötzchen behandelt wird. Eine separate MoveToTable-Aktion hält den Tisch für andere Klötzchen verfügbar.

Ein Planungsmodell definiert einen Suchraum, doch die Wahl nützlicher Aktionen bleibt schwierig. Progression sucht vorwärts durch vollständige Zustände. Regression sucht rückwärts durch die Bedingungen, die ein vorhergehender Zustand erfüllen muss. Beide können allgemeine Suchverfahren wiederverwenden und dabei die Aktionsstruktur nutzen.

Suche von beiden Enden aus

Progression beginnt beim Anfangszustand und wendet anwendbare Grundaktionen an. Sie kann Aufwand für irrelevante Aktionen verschwenden: Ein Roboter, 20 Kisten und 10 Orte ergeben schon vor der Filterung nach Anwendbarkeit 200 mögliche Pick-Grundkombinationen.

Regression betrachtet eine Aktion, die ein Zielliteral erreicht, ohne ein anderes Zielliteral zu negieren. Führe eine Zielmenge g durch a zurück, indem du erreichte Literale entfernst und Vorbedingungen hinzufügst: g′ = (g − EFFECT(a)) ∪ PRECOND(a). EFFECT enthält positive und negative Literale mit Vorzeichen. Verwirf ein inkonsistentes Ergebnis, das ein Literal und seine Negation enthält.

Für In(Box, Packing) ∧ At(R, Dock) ergibt die Regression durch Drop(R, Box, Packing) den Ausdruck Holding(R, Box) ∧ At(R, Packing) ∧ At(R, Dock). Diese Bedingungen widersprechen der beabsichtigten Invariante, dass sich der Roboter an nur einem Ort befindet. Ein gültiger Plan muss die Kiste vor der endgültigen Rückkehr des Roboters ausliefern. Die Regression durch Go(R, Shelf, Dock) ergibt stattdessen In(Box, Packing) ∧ At(R, Shelf) ∧ Connected(Shelf, Dock), wobei das ausgelieferte Paket erhalten bleibt.

Schätze die Entfernung anhand einfacherer Probleme

Eine Heuristik ist zulässig, wenn sie die verbleibenden optimalen Kosten nie überschätzt. A* mit einer zulässigen Heuristik findet einen optimalen Plan. Unerfüllte Ziele zu zählen ist nicht immer zulässig: Eine einzelne Aktion könnte mehrere erreichen.

Das Ignorieren von Vorbedingungen macht alle Aktionen sofort nutzbar. Das Ignorieren von Löscheffekten macht Fortschritt dauerhaft, wenn Probleme mit positiven Vorbedingungen und Zielen ausgedrückt werden. Negative Bedingungen müssen zuerst in ausdrücklich gepflegte positive Fluents umgewandelt werden. Die optimale relaxierte Planlänge h⁺ ist eine untere Schranke für die tatsächliche Planlänge, aber ihre Berechnung ist NP-schwer. FF findet schnell einen relaxierten Plan, ohne dessen Optimalität zu garantieren; seine Länge kann h⁺ überschätzen und ist nicht garantiert zulässig.

Für die Lagerhauslieferung mit Rückkehr als Ziel hat der tatsächliche kürzeste Plan sechs Aktionen: zu Shelf gehen, aufnehmen, zu Packing gehen, ablegen, zu Shelf zurückkehren, zu Dock zurückkehren. Die Löschrelaxation benötigt nur die ersten vier, weil At(R, Dock) nach dem Aufbruch wahr bleibt. Somit ist h⁺ = 4, während die tatsächlichen Kosten 6 betragen. Die Anzahl unerfüllter Ziele beginnt bei nur 1 und erfasst den Großteil dieser Arbeit nicht.

Kombiniere Schätzungen ohne doppelte Zählung

Ein Planungsgraph wechselt zwischen Ebenen möglicher Fluents und Aktionen; Mutex-Verbindungen markieren unvereinbare Paare. Das erste Auftreten eines Ziels liefert eine Ebenenschätzung. Das Maximum der einzelnen Zielebenen zu nehmen ist zulässig; ihre Addition kann gemeinsame Arbeit mehrfach zählen. Zustandsabstraktion entfernt einige Fluents, um den Zustandsraum zu verkleinern. Auch bei der Teilzielzerlegung hilft es, gemeinsame Aktionen zu prüfen: Das Maximum zulässiger Teilzielkosten ist unbedenklich, während ihre Summe eine zusätzliche Begründung benötigt.

Planungsverfahren unterscheiden sich darin, was sie durchsuchen: Zustände, Wahrheitsbelegungen, Reihenfolgebedingungen oder Verfeinerungen fachkundiger Vorgehensweisen. Ihr Nutzen hängt von Wechselwirkungen zwischen Teilzielen und von den Annahmen des Modells über die Ausführung ab.

Erkenne wechselwirkende Teilziele

In der Sussman-Anomalie steht C auf A, während A und B auf dem Tisch stehen. Das Ziel ist On(A, B) ∧ On(B, C). Das Teilziel A auf B zuerst zu erfüllen, blockiert das spätere Platzieren von B. B sofort auf C zu setzen lässt A begraben. Ein kürzester Plan befreit zuerst A und baut dann den Stapel von unten auf: Bewege C auf den Tisch, B auf C und dann A auf B. Die drei Züge verschränken Vorbereitung und Zielerreichung.

Kodiere einen beschränkten Plan als SAT

SATPlan wählt einen Horizont T. Es setzt Anfangsfluents zum Zeitpunkt 0, Zielfluents zu T, Aktionsvorbedingungen, Nachfolgezustandsbedingungen und Ausschlüsse für unvereinbare Aktionen voraus. Eine erfüllende Belegung wählt Aktionen aus, die einen Plan bilden. Ein unerfüllbares Ergebnis schließt Pläne innerhalb dieser Kodierung und dieses Horizonts aus.

Das Ausprobieren der Horizonte der Reihe nach findet den kleinsten erfüllbaren Horizont. Bei parallelen Aktionen minimiert dies Ebenen, nicht unbedingt die Gesamtzahl der Aktionen. Eine Abbruchschranke ist nötig, um aus wiederholt unerfüllbaren Horizonten zu schließen, dass kein Plan existiert.

Lege nur die nötige Reihenfolge fest

Partiell geordnete Planung hält Aktionen, Reihenfolgebedingungen und kausale Verknüpfungen fest. Eine Verknüpfung A -p→ B besagt, dass A die Vorbedingung p für B herstellt. Eine Aktion C, die p dazwischen löschen könnte, ist eine Bedrohung. Vorordnung setzt C vor A; Nachordnung setzt C nach B. Unabhängige Aktionen können bis zur Ausführung ungeordnet bleiben, gemäß dem Prinzip der geringstmöglichen Festlegung.

HTN-Planung verfeinert übergeordnete Aufgaben mithilfe einer Methodenbibliothek. DeliverBox kann zu einer Fahrt zur Kiste, deren Aufnahme, einer Fahrt zum Ziel und dem Ablegen werden. Diese Methoden kodieren fachkundige Vorgehensweisen, sodass sich die Suche auf nützliche Verfeinerungen konzentrieren kann, statt an jedem Punkt jede elementare Aktion zu betrachten.

Passe das Modell an die Welt an

Die Existenz eines Plans für allgemeines aussagenlogisches STRIPS ist PSPACE-vollständig. Die Klötzchenwelt hat für mögliche Anordnungen ein einfacheres Existenzproblem: Räume die Klötzchen auf den Tisch und baue neu auf, mit höchstens 2n Zügen für n Klötzchen. Einen kürzesten Plan für die Klötzchenwelt zu finden ist dennoch NP-schwer.

Klassische Modelle lassen unsichere Ergebnisse, verborgene Zustände und Aktionsdauern aus. Konformante Pläne funktionieren ohne Beobachtungen, bedingte Pläne verzweigen anhand von Beobachtungen, Online-Neuplanung reagiert auf Abweichungen bei der Ausführung und Ablaufplanung behandelt Zeiten und Ressourcen. Eine fehlende Akku-Vorbedingung kann dazu führen, dass ein im Modell gültiger Plan in der Praxis scheitert. Die Ausführungsüberwachung prüft diese Abweichung. Automatisierte Planung hat reale Systeme erreicht, darunter 1999 den Remote Agent der NASA auf Deep Space 1.