Modeling Deontic Modal Logic in ASP

Stellen Sie sich vor, Sie sind der Schiedsrichter eines riesigen, unsichtbaren Spiels namens „Was wäre wenn?“, das im Gehirn eines Computers stattfindet. In der Welt der Logik gibt es zwei Hauptwege, um über Regeln zu sprechen. Der erste ist wie eine strikte mathematische Gleichung: „Wenn A wahr ist, dann muss B wahr sein.“ Dies ist die klassische Logik, und sie ist großartig für Fakten. Aber die zweite Art ist viel menschlicher: „Du sollst B tun“, oder „Es ist verboten, A zu tun“, oder „Du darfst B tun“. Dies ist die deontische Logik (vom griechischen Wort für „Pflicht“). Es ist die Logik von Regeln, Gesetzen und moralischen Verpflichtungen. Das Schwierige ist, dass das echte Leben chaotisch ist. Manchmal ist man verpflichtet, etwas zu tun, aber man kann es nicht. Manchmal ist es verboten, etwas zu tun, aber man tut es trotzdem. Seit Jahrzehnten versuchen Informatiker und Philosophen, Computern beizubringen, wie sie mit diesen „Sollte“- und „Verboten“-Aussagen umgehen können, ohne verwirrt zu werden oder in logische Widersprüche, bekannt als Paradoxien, zu geraten.

Dieses Paper mit dem Titel „Modeling Deontic Modal Logic in ASP“ befasst sich genau mit diesem Problem. Die Autoren, ein Team von Forschern aus den USA und Spanien, schlagen einen cleveren neuen Weg vor, um Computern beizubringen, Regeln und Verpflichtungen zu verstehen. Sie verwenden eine Programmiersprache namens Answer Set Programming (ASP), die bereits berühmt für ihre Fähigkeit ist, „Was-wäre-wenn“-Szenarien und unvollständige Informationen zu handhaben. Das Paper argumentiert, dass man Regeln nicht als starre Befehle behandeln sollte, die Fakten erzwingen, sondern als globale Nebenbedingungen (wie die Pfeife eines Schiedsrichters, die ertönt, wenn eine Regel gebrochen wird), wodurch Computer endlich die jahrzehntealten Rätsel lösen können, die Logiker vor Rätsel gestellt haben. Sie zeigen, dass diese Methode berühmte logische Fallen, wie das „Contrary-to-Duty“-Paradoxon, bei dem eine Regel sich selbst zu widersprechen scheint, wenn eine Person eine vorherige Regel nicht befolgt hat, elegant löst.

Die Magie von „Sollen“ und „Müssen“

Um zu verstehen, was die Autoren getan haben, müssen wir zuerst die zwei Hauptcharaktere ihrer Geschichte kennenlernen: Verpflichtung und Erlaubnis. Im Alltag wissen wir den Unterschied zwischen „Es ist notwendig, dass die Sonne aufgeht“ (ein Naturgesetz) und „Du solltest dein Bibliotheksbuch zurückgeben“ (eine Regel, die man brechen kann). In der Welt der Logik ist das Erste alethisch (über Wahrheit und Notwendigkeit) und das Zweite deontisch (über Pflicht und Normen).

Die Autoren stellten fest, dass Computer bereits zwei spezielle Werkzeuge besitzen, um diese unterschiedlichen Arten des Denkens zu handhaben, diese aber auf die falsche Weise verwendet wurden.

1. Starke Negation: Dies ist wie ein hartes „Nein“. Wenn ein Computer sagt „Es regnet nicht“ (starke Negation), bedeutet dies, dass er den Beweis hat, dass es definitiv nicht regnet. Es ist ein Fakt.
2. Default-Negation (Negation-as-Failure): Dies ist wie ein „Vielleicht nicht“. Wenn ein Computer sagt „Es regnet nicht“ (Default-Negation), bedeutet dies lediglich, dass er keine Beweise dafür gefunden hat, dass es doch regnet. Es ist eine Vermutung basierend auf fehlenden Informationen.

Die große Idee des Papers ist es, diese beiden Computer-Werkzeuge direkt auf die zwei Arten der Logik abzubilden. Sie schlagen vor, dass wir, wenn wir über „Es ist notwendig, dass P“ (ein Fakt) sprechen, starke Negation verwenden. Aber wenn wir über „Es ist nicht notwendig, dass P“ sprechen (was bedeutet, dass P falsch sein könnte oder wir es einfach nicht wissen), verwenden wir Default-Negation. Dieser einfache Wechsel ermöglicht es dem Computer, zwischen einem harten Fakt und einer Regel, die gebrochen werden kann, zu unterscheiden.

Der „Schiedsrichter“-Ansatz

Der kreativste Teil des Papers ist die Art und Weise, wie sie Verpflichtungen handhaben. In vielen alten Systemen wurde eine Verpflichtung wie „Du musst das Auto zurückgeben“ als ein Befehl behandelt, der den Computer dazu zwingt, das Auto zurückzugeben. Aber was, wenn das Auto gestohlen wurde? Der Computer würde abstürzen, weil er das Auto nicht gewaltsam zurückgeben kann.

Die Autoren schlagen einen anderen Ansatz vor: Behandeln Sie Verpflichtungen als globale Nebenbedingungen (oder „Verneinungen“). Stellen Sie sich einen Schiedsrichter in einem Fußballspiel vor. Der Schiedsrichter zwingt die Spieler nicht, ein Tor zu schießen; der Schiedsrichter bläst einfach die Pfeife, wenn ein Foul passiert. In dem System der Autoren ist eine Verpflichtung kein Befehl, etwas wahr zu machen; es ist eine Regel, die besagt: „Wenn du dich in einer Welt befindest, in der diese Regel gebrochen wird, ist diese Welt ungültig.“

Wenn die Regel zum Beispiel lautet: „Du musst einen Sicherheitsgurt tragen“, zwingt der Computer dich nicht dazu, ihn zu tragen. Stattdessen setzt er eine Nebenbedingung: „Jede Welt, in der du ohne Sicherheitsgurt fährst, wird ausgeschlossen.“ Wenn du fährst und keinen Sicherheitsgurt hast, sagt der Computer einfach: „Dieses Szenario ist unter diesen Regeln unmöglich“, und sucht nach einem anderen Szenario, in dem du doch einen Sicherheitsgurt trägst. Aber entscheidend ist: Wenn du einen triftigen Grund hast, ihn nicht zu tragen (wie einen medizinischen Notfall), kann der Computer die Regel „voranstellen“ (preempt). Er lässt die Nebenbedingung für diese spezifische Situation weg, was es erlaubt, dass das Szenario existiert, ohne dass das System abstürzt.

Das Lösen des „Chisholm“-Rätsels

Das Paper glänzt am stärksten, wenn es das Contrary-to-Duty-Paradoxon (auch bekannt als Chisholms Paradoxon) löst. Dies ist ein berühmtes logisches Kopfzerbrechen, das so aussieht:

1. Du sollst zur Party gehen.
2. Wenn du gehst, sollst du es deiner Mutter sagen.
3. Wenn du nicht gehst, sollst du es deiner Mutter nicht sagen.
4. Du gehst nicht.

In alten Logiksystemen führt dies zu einem Chaos. Der Computer versucht herauszufinden, ob du es deiner Mutter sagen sollst oder nicht, und endet in einem Widerspruch: Du sollst ihr es sowohl sagen als als auch nicht sagen. Es ist, als bekäme ein Roboter Kopfschmerzen.

Die Autoren zeigen, dass ihre „Schiedsrichter“-Methode dies sofort löst. Sie setzen die Regeln als Nebenbedingungen auf:

• Nebenbedingung 1: Wenn du nicht gehst, kannst du es deiner Mutter nicht sagen.
• Nebenbedingung 2: Wenn du gehst, sollst du es deiner Mutter sagen.

Wenn der Computer sieht, dass du nicht gegangen bist (Fakt 4), prüft er die Nebenbedingungen. Er sieht, dass Nebenbedingung 2 (die „Wenn du gehst“-Regel) nicht zutrifft, da die Bedingung nicht erfüllt wurde. Er prüft dann Nebenbedingung 1. Da du nicht gegangen bist, besagt die Regel „Nicht sagen“. Der Computer findet problemlos eine gültige Welt, in der du nicht gegangen bist und es deiner Mutter nicht gesagt hast. Kein Widerspruch, keine Kopfschmerzen. Das „Paradoxon“ verschwindet, weil die Regeln als flexible Nebenbedingungen behandelt werden, die nur gelten, wenn ihre Bedingungen erfüllt sind, anstatt als starre Befehle, die gegeneinander kämpfen.

Warum das wichtig ist

Die Autoren lösen nicht nur ein Rätsel; sie zeigen, dass diese Methode für eine ganze Familie von logischen Problemen funktioniert, einschließlich des „Forrester-Paradoxons“ und des „Sartre-Dilemmas“. Sie demonstrieren, dass wir durch die Verwendung von Answer Set Programming mit seiner eingebauten Fähigkeit, „Was-wäre-wenn“-Szenarien und „Ausnahmen“ zu handhaben, komplexe ethische und rechtliche Systeme viel natürlicher modellieren können als zuvor.

Sie zeigen auch, wie dies mit „sekundären Verpflichtungen“ umgeht. Stell dir vor, du leihst dir das Auto eines Freundes. Du hast eine Hauptregel: „Gib das Auto zurück.“ Aber es gibt sekundäre Regeln: „Gib es vor Mittag zurück“ und „Gib es mit vollem Akku zurück.“ Wenn du das Auto gegen die Wand fährst (eine Verletzung der Hauptregel), könnten sich die sekundären Regeln ändern oder verschwinden. Die Autoren zeigen, wie ihr System diese Regeln automatisch „voranstellen“ (preempt) kann. Wenn das Auto zerstört ist, wird die Nebenbedingung „Gib es vor Mittag zurück“ fallen gelassen, weil die Bedingung (ein Auto zu besitzen, das man zurückgeben kann) nicht mehr gegeben ist. Der Computer wird nicht verwirrt; er aktualisiert einfach die Liste der gültigen Welten.

Das Fazbeit

Dieses Paper behauptet nicht, jedes Problem in Ethik oder Recht gelöst zu haben. Stattdessen bietet es ein sauberes, elegantes Werkzeugset für den Bau von Systemen, die Regeln verstehen. Es beweist, dass wir, indem wir „Sollen“ als Nebenbedingungen für mögliche Welten behandeln anstatt als Befehle, die die Realität verändern, Computer bauen können, die über Regeln so denken wie Menschen: flexibel, mit Ausnahmen und ohne in logischen Schleifen stecken zu bleiben. Die Autoren legen nahe, dass dieser Ansatz einfacher und direkter ist als bisherige Methoden, die oft komplexe neue Mathematik oder „Sanktionen“ (Bestrafungen) erforderten, um die Logik zum Laufen zu bringen. Durch die Nutzung der Werkzeuge, die bereits in der Answer Set Programming verfügbar sind, haben sie gezeigt, dass der Weg zum Verständnis menschlicher Regeln kürzer und geradliniger sein könnte, als wir dachten.