Agentive Logic, auch als Logik des Handelns oder Logik der Handlungsfähigkeit bezeichnet, ist ein Zweig der philosophischen Logik und der Logik in der Informatik, der formale Darstellungen von Agenten, ihren Handlungen und ihren Fähigkeiten untersucht. Im engeren Sinne ist eine Agentive Logic ein formales System, dessen primitive Operatoren ausdrücken, dass ein Agent etwas tut, etwas tun kann oder dafür sorgt, dass etwas der Fall ist. Diese Logiken verallgemeinern die Modallogik, indem sie Modalitäten hinzufügen, die auf Agenten und Handlungen indexiert sind, und ermöglichen präzises Schließen darüber, was Agenten erreichen können, wie ihre Entscheidungen interagieren und was sie bewirken.
Das Feld hat Wurzeln in der mittelalterlichen Philosophie und der modernen Logik und ist zentral für Bereiche wie künstliche Intelligenz, Programmverifikation und die Semantik natürlicher Sprache geworden. Agentive Logiken bieten einen rigorosen Rahmen für die Modellierung intelligenter Agenten, Planungssysteme und Multi-Agenten-Interaktionen, was sie sowohl für theoretische als auch für angewandte Arbeiten in der Informatik unverzichtbar macht.
Terminologie und Umfang
Das Adjektiv „agentiv“ leitet sich vom lateinischen agens („der Handelnde“) ab und bezog sich ursprünglich auf das grammatische Agens eines Verbs. In logischen Kontexten bezeichnet es Operatoren oder Prädikate, deren primäre Argumentposition ein Agent ist und nicht nur eine Proposition, zum Beispiel \(A_i\varphi\) („Agent \(i\) tut \(\varphi\)“) oder \(C_i\varphi\) („Agent \(i\) kann \(\varphi\) bewirken“).
In der zeitgenössischen Literatur wird Agentive Logic manchmal eng für formale Rekonstruktionen von St. Anselms modaler Darstellung von facere („tun“) verwendet. Weiter gefasst wird der Begriff synonym mit Logik des Handelns oder Logik der Handlungsfähigkeit verwendet, um eine Familie von modalen und dynamischen Logiken abzudecken, die darauf ausgelegt sind, die Struktur von Handlung und Wahl zu erfassen. Diese breitere Verwendung umfasst Systeme, die in Philosophie, Linguistik und Informatik entwickelt wurden, die alle einen Fokus auf Agenten als explizite Elemente der logischen Form teilen.
Historischer Hintergrund
Mittelalterliche und frühneuzeitliche Wurzeln
Mittelalterliche Logiker untersuchten bereits Analogien zwischen Handlungsmodalitäten und alethischen Modalitäten wie Möglichkeit und Notwendigkeit, insbesondere in Diskussionen über Verpflichtung und Macht. Eine einflussreiche frühe agentive Analyse stammt von St. Anselm (11. Jahrhundert), der „\(\varphi\) tun“ als eine Art modalen Operator auf Propositionen behandelte und damit spätere modale Logiken der Handlungsfähigkeit vorwegnahm. Moderne Rekonstruktionen von Anselms Theorie zeigen, dass die resultierende Agentive Logic mit Nachbarschaftssemantik modelliert werden kann und ein erkennbares logisches Quadrat der Opposition erfüllt.
Moderne Logik des Handelns
Die moderne Untersuchung der Logik des Handelns begann Mitte des 20. Jahrhunderts, parallel zu Entwicklungen in der deontischen Logik und der Zeitlogik. Frühe Systeme wurden von Georg Henrik von Wright, Stig Kanger und anderen vorgeschlagen, oft motiviert durch Fragen zu Normen und Verantwortung. Ab den 1960er Jahren entstanden zwei weitgehend unabhängige, aber schließlich konvergierende Traditionen: eine Verzweigungszeit-Tradition, die in STIT-Logiken gipfelte und die Entscheidungen von Agenten zwischen möglichen Zukünften betonte, sowie dynamische Logiken von Programmen und Handlungen, die in der Informatik entwickelt wurden, um über Programmausführung zu schließen.
In den 1990er und 2000er Jahren wurden Handlungslogiken weiterentwickelt in Verbindung mit Wissensrepräsentation, Planung und Multi-Agenten-Systemen in der KI sowie mit dynamischer und Updatesemantik in der Linguistik. Diese Entwicklungen integrierten Erkenntnisse aus Philosophie, theoretischer Informatik und KI und schufen ein reichhaltiges interdisziplinäres Feld.
Kernideen
Trotz ihrer Vielfalt teilen die meisten Agentive Logiken mehrere allgemeine Themen. Agenten werden als explizite Indizes modaler Operatoren behandelt, wie in \([i\ {\sf does}]\varphi\) oder \(C_i\varphi\). Handlungen werden entweder implizit dargestellt, über Veränderungen zwischen möglichen Welten entlang einer Erreichbarkeitsrelation, oder explizit, als Terme, die primitive und zusammengesetzte Handlungen bezeichnen. Wahl und Fähigkeit werden durch Modalitäten erfasst, die beschreiben, was ein Agent sicherstellen kann, normalerweise relativ zu Annahmen über die Umgebung und andere Agenten.
Formale Eigenschaften wie Abschluss unter Komposition, Interaktion zwischen verschiedenen Agenten und Verbindungen zu Verpflichtung (was ein Agent tun sollte) und Wissen (was ein Agent zu tun weiß) werden untersucht. Diese Kernideen bieten einen gemeinsamen Rahmen für den Vergleich verschiedener Systeme und für ihre Anwendung auf praktische Probleme.
STIT-Logiken
STIT-Logiken („sees to it that“), die auf Arbeiten von Nuel Belnap und Mitarbeitern zurückgehen, behandeln Handlungsfähigkeit in einem Verzweigungszeit-Rahmen. Ein STIT-Modell besteht aus einer teilweise geordneten Menge von Momenten mit einer baumartigen Struktur, Mengen von Historien (maximale Zweige durch den Baum) und für jeden Agenten zu jedem Moment einer Partition der Historien durch diesen Moment, die die dem Agenten verfügbaren Entscheidungen darstellt.
Intuitiv bestimmt die Handlung eines Agenten zu einem Moment, welche Äquivalenzklasse (Entscheidungszelle) von Historien tatsächlich wird; eine Formel \([i\ {\sf stit}:\varphi]\) ist an einem Historien-Moment-Paar wahr, wenn \(\varphi\) auf allen Historien in der Entscheidungszelle gilt, die der aktuellen Handlung des Agenten entspricht. Verschiedene STIT-Operatoren wurden unterschieden, insbesondere der Chellas-STIT-Operator, oft geschrieben als \([i\ {\sf cstit}:\varphi]\), und der deliberative STIT-Operator, der die Bedingung hinzufügt, dass die Entscheidung des Agenten einen Unterschied für die Wahrheit von \(\varphi\) macht. Diese Operatoren ermöglichen präzises Schließen über individuelle und gemeinsame Handlungsfähigkeit, einschließlich Fällen, in denen Agenten zusammen handeln oder in denen die Handlung eines Agenten die eines anderen ausschließt.
STIT-Logiken wurden auf deontisches Schließen, Spieltheorie und die Analyse von Verantwortung und Kausalität angewendet. Sie bieten einen robusten Rahmen für die Modellierung von Wahl und Fähigkeit in dynamischen Umgebungen und haben Arbeiten an Multi-Agenten-Systemen in KI beeinflusst.
Dynamische Logiken des Handelns
Dynamische Logiken, die ab den 1970er Jahren in der Informatik entwickelt wurden, stellen Handlungen als Programme mit Modalitäten \([\alpha]\varphi\) und \(\langle\alpha\rangle\varphi\) dar, was grob bedeutet, dass nach jeder (bzw. einigen) Ausführung(en) der Handlung \(\alpha\), \(\varphi\) gilt. Diese Logiken wurden ursprünglich für die Programmverifikation entwickelt und ermöglichen das Schließen über die Auswirkungen von Programmausführung auf Zustände.
In agentiven Kontexten werden dynamische Logiken verwendet, um Handlungen explizit als Terme zu modellieren, mit Operatoren für Komposition, Wahl und Iteration. Dies ermöglicht die Darstellung komplexer Handlungsstrukturen, wie Sequenzen von Handlungen, bedingte Handlungen und wiederholte Handlungen. Dynamische Logiken des Handelns wurden auf Planung, Robotik und die Semantik natürlicher Sprache angewendet, wo sie die Bedeutung von Handlungssätzen und Imperativen erfassen.
Anwendungen in der künstlichen Intelligenz
Agentive Logiken untermauern Formalismen für das Schließen über Handlungen, Planung und intelligente Agenten in künstlicher Intelligenz. Sie bieten eine formale Grundlage für die Darstellung des Wissens, der Fähigkeiten und der Ziele eines Agenten sowie für das Schließen darüber, wie Handlungen die Welt verändern. In der Planung helfen Agentive Logiken, Vorbedingungen und Effekte von Handlungen zu spezifizieren, und unterstützen das Schließen über alternative Pläne und ihre Ergebnisse.
In Multi-Agenten-Systemen modellieren Agentive Logiken Interaktionen zwischen Agenten, einschließlich Kooperation, Wettbewerb und Kommunikation. Sie werden verwendet, um Protokolle zu spezifizieren, Eigenschaften verteilter Systeme zu verifizieren und strategisches Verhalten zu analysieren. Die Entwicklung großer Sprachmodelle und anderer maschineller Lernsysteme hat ebenfalls auf agentive Konzepte zurückgegriffen, da Forscher Agenten bauen möchten, die über ihre eigenen Handlungen und die anderer schließen können.
Beziehung zu anderen Logiken
Agentive Logiken sind eng mit Modallogiken, deontischen Logiken und temporalen Logiken verwandt. Sie erweitern die Modallogik, indem sie agentenindizierte Modalitäten hinzufügen, und integrieren oft temporale Operatoren, um Veränderungen über die Zeit darzustellen. Deontische Logiken, die über Verpflichtung und Erlaubnis schließen, können mit Agentive Logiken kombiniert werden, um auszudrücken, was ein Agent tun sollte oder darf. Temporale Logiken, wie lineare temporale Logik und Computation Tree Logic, bieten eine Grundlage für das Schließen über Handlungssequenzen und verzweigte Zukünfte.
Die Verbindungen zwischen Agentive Logiken und Wissen sind ebenfalls wichtig. Epistemische Logiken, die darüber schließen, was Agenten wissen, können mit Agentive Logiken integriert werden, um auszudrücken, was ein Agent zu tun weiß oder weiß, dass er es erreichen kann. Diese Integration ist entscheidend für Anwendungen in der KI, wo Agenten über ihr eigenes Wissen und ihre Fähigkeiten schließen müssen.
Siehe auch
- Modallogik
- Deontische Logik
- Temporale Logik
- Multi-Agenten-System