🔢 mathematics

Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof

Diese Arbeit liefert einen konstruktiven Beweis dafür, dass die Propositional Dynamic Logic (PDL) die Craig-Interpolations-Eigenschaft besitzt, indem sie ein zyklisches Tableau-System mit einem Lade-Mechanismus sowie eine modifizierte Methode nach Maehara zur Berechnung von Interpolanten verwendet und damit ein langjähriges offenes Problem löst, nachdem frühere Versuche zurückgezogen oder kritisiert wurden.

Ursprüngliche Autoren: Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema

Veröffentlicht 2026-08-12

📖 3 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie sind ein Detektiv, der versucht, ein Rätsel zu lösen, aber Sie dürfen nur einen ganz bestimmten Satz an Hinweisen verwenden. Sie haben einen langen, komplizierten Bericht von einem Zeugen (nennen wir ihn „den Ankläger“) und einen Gegenbericht von einem anderen („den Verteidiger“). Ihre Aufgabe ist es, einen einzigen, kurzen Satz zu finden, der den Konflikt zwischen ihnen erklärt. Dieser Satz muss der „Mittelweg“ sein: Er muss wahr sein, wenn der Ankläger recht hat, und er muss falsch sein, wenn der Verteidiger recht hat. Entscheidend ist, dass dieser Satz nur Wörter verwenden darf, die in beiden Berichten vorkommen. Wenn der Ankläger von „Katzen“ und „Mäusen“ spricht und der Verteidiger von „Hunden“ und „Knochen“, darf Ihr Mittelsatz weder „Katzen“ noch „Knochen“ erwähnen; er darf nur Wörter wie „Tiere“ oder „jagen“ verwenden, wenn diese Wörter in beiden Geschichten vorkommen. In der Welt der Informatik wird dieses Detektivspiel Craig-Interpolations-Eigenschaft genannt. Es ist eine Superkraft, die Computern hilft zu verstehen, wie verschiedene Teile eines Systems miteinander zusammenhängen, ohne sie durch irrelevante Details zu verwirren.

Das spezifische Detektivspiel, das dieses Papier behandelt, beinhaltet die Propositionale Dynamische Logik (PDL). Denken Sie an PDL als eine Sprache, die beschreibt, wie Computerprogramme sich verhalten. Es ist wie ein Regelwerk für ein Videospiel, das sagt: „Wenn du ‚A‘ drückst, dann ‚B‘, dann springst du“, oder „Wenn du ‚X‘ immer wieder drückst, wirst du schließlich fliegen“. Der schwierige Teil ist das „schließlich“ oder das „dies ewig fortführen“ – was die Logik sehr mächtig, aber auch sehr schwer lösbar macht. Jahrzehntelang haben Mathematiker und Informatiker versucht, zu beweisen, dass dieses spezielle Regelwerk (PDD) über die Superkraft der Interpolation verfügt. Drei verschiedene Teams haben versucht, das Rätsel zu lösen, aber ihre Lösungen wurden als lückenhaft befunden, was die Frage offen und frustrierend ließ.

Dieses Papier löst das Rätsel schließlich. Die Autoren, ein Team von Forschern aus Deutschland und den Niederlanden, haben einen brandneuen, strengen Beweis konstruiert, dass die Propositionale Dynamische Logik tatsächlich die Craig-Interpolations-Eigenschaft besitzt. Sie haben nicht nur geraten; sie haben ein spezielles Werkzeug namens „zyklisches Tableau-System“ gebaut. Stellen Sie sich dieses System als einen riesigen, verzweigenden Baum vor, in dem Sie versuchen, ein komplexes Logikrätsel in immer kleinere Teile zu zerlegen. Normalerweise wachsen diese Bäume ewig weiter, aber die Autoren haben einen speziellen „Lademodus“ hinzugefügt, der wie ein Sicherheitsnetz fungiert. Wenn der Baum beginnt, sich selbst zu kreisen (was passiert, wenn Programme Aktionen wiederholen), erkennt dieser Mechanismus die Schleife und stoppt das Wachstum, wodurch sichergestellt wird, dass der Beweis endlich und handhabbar bleibt.

Mit diesem neuen Baum-Bau-Werkzeug haben die Autoren gezeigt, dass man für jede gültige logische Aussage in der PDL immer diesen perfekten „Mittelsatz“ (den Interpolanten) finden kann, der zwei Seiten eines Arguments unter Verwendung ihres gemeinsamen Wortschatzes verbindet. Sie haben nicht nur bewiesen, dass er existiert; sie haben genau gezeigt, wie man ihn berechnet. Sie haben sogar ein Computerprogramm in einer Sprache namens Haskell geschrieben, das diese Berechnung für Sie durchführen kann, und sie arbeiten derzeit an einer zweiten Ebene des Beweises unter Verwendung eines digitalen Assistenten namens „Lean“, um zu verifizieren, dass ihre Mathematik zu 100 % korrekt ist. Während sie das Haupträtsel gelöst haben, geben sie zu, dass einige kleinere, verwandte Fragen – wie etwa, ob dies für eine vereinfachte Version der Logik ohne „Test“-Befehle funktioniert – offen bleiben, um von zukünftigen Detektiven gelöst zu werden. Aber für den Moment ist die große Frage beantwortet: PDL besitzt die Superkraft der Interpolation, und wir wissen nun genau, wie wir sie anwenden können.

Technisches Resümee: Propositionale Dynamische Logik besitzt die Craig-Interpolation

1. Das Problem

Die Arbeit befasst sich mit der langjährigen offenen Frage, ob die Propositionale Dynamische Logik (PDL) die Eigenschaft der Craig-Interpolation besitzt. Die Craig-Interpolation (CIP) besagt, dass für jede gültige Implikation $\phi \to \psi$ ein Interpolant $\theta$ existiert, so dass $\phi \to \theta$ und $\theta \to \psi$ gültig sind und $\theta$ nur propositionale Variablen und atomare Programme enthält, die sowohl in $\phi$ als auch in $\psi$ vorkommen.

Obwohl die PDL eine gut untersuchte Modallogik mit etablierten Entscheidbarkeits- und Vollständigkeitsergebnissen ist, blieb ihr Interpolationsstatus jahrzehntelang ungeklärt. In der Literatur finden sich drei frühere Versuche, die Interpolation zu beweisen:

Leivant (1981): Behauptete einen Beweis, der später von Kracht (1999) aus falschen Gründen widerlegt wurde, obwohl eine echte Lücke in Leivants Beweis bestehen bleibt.
Borzechowski (1988): Eine Diplomarbeit, die einen Beweis behauptete, der jedoch wenig Beachtung fand und von einigen als nicht verifizierbar abgetan wurde.
Kowalski (2002): Behauptete einen Beweis, der widerlegt wurde und 2004 offiziell zurückgezogen wurde.

Die Schwierigkeit ergibt sich daraus, dass die PDL eine modale Fixpunktlogik ist (aufgrund des Iterationsoperators $*$ ). Während die Interpolation für die vollständige $\mu$ -Kalkül und deren alternationsfreie Fragmente mittels zyklischer Beweissysteme etabliert wurde, machen die spezifischen Einschränkungen der PDL es schwierig sicherzustellen, dass die Lösungen der durch die Interpolanten charakterisierten Fixpunktgleichungen innerhalb der PDL ausdrückbar sind, anstatt die volle Ausdrucksstärke des $\mu$ -Kalküls zu erfordern.

2. Methodik

Die Autoren liefern einen konstruktiven Beweis basierend auf einem zyklischen Tableau-System und einer Adaption von Maehara's beweistheoretischer Methode.

2.1. Ein zyklisches Tableau-System für PDL

Die Autoren definieren ein neues Tableau-System für die PDL, das auf gespaltenen Sequenzen (Paaren von Formelsätzen) operiert. Wesentliche Merkmale sind:

Lokales vs. Modales Schließen: Das System unterscheidet zwischen lokalen Regeln (propositionale Logik und Entfaltung von Programmen innerhalb eines einzelnen Zustands) und modalen Regeln (Bewegung zwischen Zuständen in einem Kripke-Modell).
Entfaltungsmechanismus: Anstatt Standard-Reduktionsregeln für jeden Programmkonstruktor zu verwenden, nutzt das System einen „Lade“-Mechanismus (loading mechanism). Formeln der Form $[\alpha]\psi$ (wobei $\alpha$ nicht-atomar ist) werden baserausgehend auf „Testprofilen“ in eine endliche Menge von Sequenzen entfaltet. Diese Menge, bezeichnet als $\text{unfold}_\square(\alpha, \psi)$ , repräsentiert die Disjunktion aller möglichen Ausführungspfade von $\alpha$ , bei denen spezifische Tests erfolgreich oder erfolglos sind.
Umgang mit Iteration: Um eine unendliche lokale Entfaltung von Formeln wie $[\alpha^*]\psi$ zu verhindern, eliminiert das System regenerierte Vorkommen der Formel während des Entfaltungsprozesses. Dies stützt sich auf die Beobachtung, dass $[\alpha^*]\psi$ ein größter Fixpunkt ist.
Zyklische Beweise: Das System erlaubt „Wiederholungen“ (Repeats) (Knoten mit identischen Labels wie einem Vorfahren).
- Geladene Pfad-Wiederholungen (Loaded-path repeats): Eine Wiederholung, bei der der Pfad vom Vorfahren (Companion) zum aktuellen Knoten ausschließlich aus geladenen Knoten besteht. Diese werden als „erfolgreiche“ Blätter behandelt (was einen Loop anzeigt, der die Formel erfüllt).
- Freie Wiederholungen (Free repeats): Eine Wiederholung, bei der der Pfad ungeladene Knoten enthält. Diese werden als „unerfolgreiche“ Blätter behandelt, was auf ein potenzielles Gegenmodell hindeutet.
Terminierung: Das System gewährleistet Endlichkeit, indem es erzwingt, dass alle freien Wiederholungen und geladenen Pfad-Wiederholungen Blätter sind, und indem es den Fischer-Ladner-Abschluss zur Begrenzung der Formelmenge nutzt.

2.2. Interpolation via Quasi-Tableaux und Fixpunktgleichungen

Um den Interpolanten zu konstruieren, adaptieren die Autoren Maehara's Methode für den zyklischen Kontext:

Cluster: Das Tableau wird als Graph betrachtet, der Rückwärtskanten von Wiederholungen zu Companions besitzt. Die stark zusammenhängenden Komponenten (SCCs) dieses Graphen werden als „Cluster“ bezeichnet.
Quasi-Tableaux: Für einen echten Cluster (eine nicht-einzelne SCC) definieren die Autoren ein „Quasi-Tableau“. Diese Struktur wird verwendet, um ein System von Gleichungen aufzustellen, die den Interpolanten charakterisieren.
Pre-Interpolanten: Die Methode definiert „Pre-Interpolanten“ für Knoten im Quasi-Tableau via Blatt-zu-Wurzel-Induktion.
- Bei Exit-Knoten (Blätter, die nicht Teil des Clusters sind) ist der Pre-Interpolant der Interpolant des Exit-Knotens (existiert induktiv vorausgesetzt).
- Bei Repeat-Blättern ist der Pre-Interpolant eine interne propositionale Variable $q_x$ .
- Bei Companion-Knoten ist der Pre-Interpolant als Lösung einer Fixpunktgleichung definiert. Speziell: Wenn ein Companion $x$ ein Kind $y$ mit Pre-Interpolant $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$ hat, ist der Pre-Interpolant für $x$ definiert als $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$ .
Lösen in PDL: Die entscheidende Erkenntnis ist, dass diese spezifische Konstruktion sicherstellt, dass die Lösungen der Fixpunktgleichungen innerhalb der Sprache der PDL bleiben. Die Verwendung des Iterationsoperators $*$ in der Definition von $\iota_x$ löst effektiv die Gleichung $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ innerhalb der PDL.
Finaler Interpolant: Der Interpolant für die Wurzel des Clusters wird durch Substitution der internen Variablen im Pre-Interpolanten der Wurzel mit den entsprechenden Regionenformeln (Disjunktionen der linken Seiten der gespaltenen Sequenzen) erhalten.

3. Zentrale Beiträge und Ergebnisse

Beweis der CIP für PDL: Die Arbeit etabliert, dass die PDL die Eigenschaft der Craig-Interpolation besitzt.
Beth-Definierbarkeit: Als Korollar beweist die Arbeit, dass die PDL die Beth-Definierbarkeit besitzt (da CIP in Gegenwart eines Deduktionstheorems die Beth-Definierbarkeit impliziert).
Konstruktiver Algorithmus: Der Beweis ist konstruktiv. Die Autoren stellen einen klaren Algorithmus zur Berechnung von Interpolanten aus einem geschlossenen Tableau bereit.
Formale Verifikation: Die Autoren haben den Beweis teilweise im interaktiven Theoremprover Lean 4 formalisiert. Zum Zeitpunkt der Niederschrift der Arbeit wurden die Sätze über Korrektheit (Soundness) und Vollständigkeit (Completeness) sowie mehrere unterstützende Lemmata verifiziert.
Implementierung: Eine Haskell-Implementierung des Tableau-Systems und der Interpolanten-Konstruktion wird bereitgestellt und ist über eine Weboberfläche verfügbar.

4. Bedeutung und Ansprüche

Die Arbeit beansprucht, ein Rätsel in der Literatur bezüglich des Interpolationsstatus der PDL zu lösen, indem sie den ersten verifizierten Beweis liefert, der die Lücken früherer Versuche überwindet.

Klärung historischer Probleme: Die Autoren adressieren explizit die Geschichte gescheiterter Versuche und merken an, dass ihr Ansatz auf den Kernideen von Borzechowski (1988) aufbaut, aber die Handhabung zyklischer Beweise und die Konstruktion von Interpolanten innerhalb der Sprache der PDL rigoros formalisiert.
Methodische Neuheit: Die Arbeit hebt hervor, dass während Maehara's Methode für nicht-zyklische Beweise Standard ist, die Anwendung auf zyklische Beweise (Fixpunktlogiken) das Lösen von Fixpunktgleichungen erfordert. Die Autoren zeigen, dass für die PDL diese Lösungen unter Verwendung des eigenen Iterationsoperators der Logik ausdrückbar sind – ein nicht triviales Ergebnis, das die PDL von anderen Fragmenten unterscheidet, bei denen solche Lösungen den vollen $\mu$ -Kalkül erfordern könnten.
Offene Fragen: Die Autoren merken bescheiden an, dass ihre Methode auf der Präsenz von Test-Programmen ( $\tau?$ ) beruht. Folglich bleibt die Frage offen, ob das testfreie Fragment der PDL Interpolation besitzt, da ihre Konstruktion im Allgemeinen Interpolanten enthält, die Tests enthalten, selbst wenn die Eingabe testfrei ist. Sie lassen zudem die Erweiterung ihrer Methode auf andere PDL-Varianten (z. B. mit Konvers oder Intersektion) sowie die Implikationen für Kleene-Algebren mit Tests (KAT) als offene Fragen offen.

Zusammenfassend liefert die Arbeit einen definitiven, konstruktiven Beweis der Craig-Interpolation für die PDL unter Verwendung eines neuartigen zyklischen Tableau-Systems und einer spezialisierten Fixpunkt-Lösungstechnik für Interpolanten, gestützt durch eine Haskell-Implementierung und eine teilweise formale Verifikation in Lean.