Epistemische Modallogik ist ein Zweig der Modallogik, der das Schließen über Wissen und Glauben formalisiert. Sie erweitert die Aussagenlogik um modale Operatoren, die ausdrücken, was einzelne Agenten wissen oder glauben, und ermöglicht so eine präzise Analyse von Aussagen wie „Agent A weiß, dass die Aussage P gilt" oder „Agent B glaubt, dass Agent A P weiß". Der Rahmen entstand in der Philosophie, ist aber zu einem zentralen Werkzeug in Informatik, Wirtschaftswissenschaft und künstlicher Intelligenz geworden, um Multi-Agenten-Systeme, verteilte Protokolle und spieltheoretische Szenarien zu modellieren.
Die formale Sprache der epistemischen Modallogik umfasst typischerweise eine Menge von Aussagenvariablen, boolesche Verknüpfungen und modale Operatoren K_i für jeden Agenten i, wobei K_i φ als „Agent i weiß, dass φ" gelesen wird. In Multi-Agenten-Systemen fügt man oft Operatoren für gemeinsames Wissen (C_G φ) und verteiltes Wissen (D_G φ) für eine Gruppe G hinzu. Die Standard-Semantik, die Saul Kripke Ende der 1950er Jahre einführte und Robert Aumann 1976 verfeinerte, verwendet Kripke-Frames, die aus einer Menge möglicher Welten und einer Äquivalenzrelation für jeden Agenten bestehen. Eine Formel K_i φ ist an einer Welt w wahr, wenn φ in allen Welten gilt, die Agent i von w aus für möglich hält.
Axiomensysteme
Die gebräuchlichste epistemische Logik, bekannt als S5, wird durch die folgenden Axiome und Regeln charakterisiert. Das Axiom K besagt, dass ein Agent, der eine Implikation kennt und deren Antezedens kennt, auch das Konsequens kennt: K_i(φ → ψ) → (K_i φ → K_i ψ). Das Axiom T besagt, dass Wissen Wahrheit impliziert: K_i φ → φ. Das Axiom 4 (positive Introspektion) besagt, dass ein Agent, der φ kennt, auch weiß, dass er φ kennt: K_i φ → K_i K_i φ. Das Axiom 5 (negative Introspektion) besagt, dass ein Agent, der φ nicht kennt, auch weiß, dass er φ nicht kennt: ¬K_i φ → K_i ¬K_i φ. Die Regel der Notwendigkeit erlaubt es, K_i φ aus einem Theorem φ abzuleiten.
Schwächere Systeme lockern diese Axiome. Die Logik KT (auch T genannt) verwirft die Axiome 4 und 5 und erlaubt Agenten, keine Introspektion zu besitzen. Die Logik S4 behält Axiom 4 bei, verwirft aber Axiom 5, was oft für Glauben statt Wissen verwendet wird. Für Glauben wird das Axiom T durch das Axiom D ersetzt: B_i φ → ¬B_i ¬φ, das besagt, dass Überzeugungen konsistent, aber nicht notwendigerweise wahr sind. Diese Unterscheidungen sind in Anwendungen wichtig, in denen Agenten unvollständige oder falsche Informationen haben.
Semantik und mögliche Welten
Die Semantik der möglichen Welten interpretiert Wissen als Wahrheit in allen epistemisch zugänglichen Welten. Ein epistemisches Modell M = (W, R_1, ..., R_n, V) besteht aus einer Menge von Welten W, einer Zugänglichkeitsrelation R_i für jeden Agenten und einer Bewertung V, die Aussagenvariablen an jeder Welt Wahrheitswerte zuweist. Für Wissen ist jedes R_i eine Äquivalenzrelation (reflexiv, symmetrisch, transitiv), was widerspiegelt, dass Agenten Welten, die epistemisch identisch für sie sind, nicht unterscheiden können. Die Wahrheitsbedingung für K_i φ an Welt w lautet: für alle v mit w R_i v gilt M, v ⊨ φ.
Gemeinsames Wissen, formalisiert von David Lewis 1969 und Robert Aumann 1976, ist definiert als die unendliche Konjunktion von „jeder weiß, dass jeder weiß ...". Für eine Gruppe G gilt C_G φ, wenn φ in allen Welten wahr ist, die durch eine endliche Folge von Zugänglichkeitsrelationen für Mitglieder von G erreichbar sind. Dieses Konzept ist entscheidend für koordiniertes Handeln in verteilten Systemen und für die Analyse von Vereinbarungen und Konventionen.
Anwendungen in Informatik und KI
Epistemische Logik wurde in den 1980er und 1990er Jahren zu einem Eckpfeiler der Forschung an Multi-Agenten-Systemen. 1985 veröffentlichten Joseph Halpern und Yoram Moses grundlegende Arbeiten über Wissen und gemeinsames Wissen in verteilten Systemen und zeigten, wie epistemische Bedingungen die Lösbarkeit von Koordinationsproblemen wie dem Problem des koordinierten Angriffs charakterisieren. Das Rätsel der schmutzigen Kinder, ein klassisches Beispiel, zeigt, wie öffentliche Bekanntgaben von Unwissen gemeinsames Wissen erzeugen und das Schließen über Wissen höherer Ordnung ermöglichen können.
In der künstlichen Intelligenz bietet epistemische Logik eine formale Grundlage für Wissensrepräsentation und Schließen. Sie wurde angewendet, um wissensbasierte Programme zu modellieren, bei denen die Aktionen von Agenten von ihren Wissenszuständen abhängen. Der Rahmen liegt auch der epistemischen Planung zugrunde, bei der Agenten darüber nachdenken, was andere wissen, um Ziele zu erreichen. In der Spieltheorie zeigte Aumanns Ergebnis von 1976 über das „Agreeing to Disagree", dass Agenten, die gemeinsames Wissen über die Posteriori-Überzeugungen des jeweils anderen haben, nicht vereinbaren können, anderer Meinung zu sein, was epistemische Logik mit wirtschaftlichem Denken verbindet.
Dynamische epistemische Logik
Dynamische epistemische Logik (DEL), entwickelt von Jan Plaza 1989 und später erweitert von Hans van Ditmarsch, Wiebe van der Hoek und Barteld Kooi, fügt Operatoren für Wissensänderung durch öffentliche Bekanntgaben oder private Kommunikation hinzu. Eine öffentliche Bekanntgabe von φ transformiert das Modell, indem alle Welten entfernt werden, in denen φ falsch ist, und der Bekanntgabeoperator [φ!]ψ besagt, dass ψ nach der Bekanntgabe gilt. Dieser Rahmen erfasst Phänomene wie die Effekte der Offenlegung von Informationen, Lügen und Täuschung in Multi-Agenten-Umgebungen.
DEL wurde angewendet, um Kommunikationsprotokolle, Sicherheitsprotokolle und soziale Interaktionen zu modellieren. Zum Beispiel kann die Logik öffentlicher Bekanntgaben ausdrücken, dass Agenten nach einer wahrheitsgemäßen Bekanntgabe von φ ihr Wissen entsprechend aktualisieren, was potenziell neues gemeinsames Wissen erzeugt. Der Rahmen behandelt auch komplexere Aktionen wie private Nachrichten und gleichzeitige Bekanntgaben, was ihn zu einem reichhaltigen Werkzeug für die Analyse von Informationsfluss macht.
Neuere Entwicklungen und Herausforderungen
Epistemische Logik entwickelt sich weiter mit Verbindungen zu Spieltheorie, Kausalität und maschinellem Lernen. Forscher haben epistemische Bedingungen für faire Verteilung, Privatsphäre und Sicherheit in Multi-Agenten-Systemen untersucht. Die Kombination von epistemischer Logik mit Wahrscheinlichkeit, wie in der probabilistischen epistemischen Logik, erlaubt das Schließen über Grade von Glauben und Wissen unter Unsicherheit. Dies hat Anwendungen in der Entscheidungstheorie und bei der Modellierung von KI-Systemen, die probabilistische Überzeugungen über ihre Umgebungen aufrechterhalten.
Eine offene Herausforderung ist die rechnerische Komplexität von Model Checking und Erfüllbarkeit in epistemischen Logiken. Für S5 mit mehreren Agenten ist die Erfüllbarkeit PSPACE-vollständig, während Model Checking für feste Formeln in polynomieller Zeit durchgeführt werden kann. Dynamische epistemische Logiken haben oft höhere Komplexität, wobei einige Varianten unentscheidbar sind. Diese Komplexitätsergebnisse leiten das Design praktischer Schließwerkzeuge und begrenzen die Skalierbarkeit formaler Verifikation in großen Multi-Agenten-Systemen.
Im Kontext moderner KI bietet epistemische Logik eine formale Sprache zur Spezifikation dessen, was ein KI-System weiß oder nicht weiß, was für Transparenz und Robustheit relevant ist. Forscher an Institutionen wie dem Stanford AI Lab und BAIR (Berkeley AI Research) haben Verbindungen zwischen epistemischer Logik und Machine learning-Modellen untersucht, insbesondere bei Aufgaben, die Large language model-Schließen über Wissen und Unsicherheit betreffen. Diese Anwendungen bleiben jedoch ein aktives Forschungsgebiet, und die direkte Integration epistemischer Logik in Deep-Learning-Systeme ist Stand 2025 noch in den Anfängen.
Siehe auch
- Multi-Agenten-System
- Wissensrepräsentation
- Modallogik
- Spieltheorie
- Formale Verifikation