🔢 mathematics

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

Dit artikel levert een constructief bewijs dat de Propositielogica van Dynamische Logica (PDL) de Craig-interpolatie-eigenschap bezit door een cyclisch tableau-systeem met een laadmechanisme en een aangepaste methode van Maehara te gebruiken om interpolanten te berekenen, waarmee een langdurig openstaand probleem wordt opgelost nadat eerdere pogingen werden ingetrokken of bekritiseerd.

Oorspronkelijke auteurs: Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema

Gepubliceerd 2026-08-12

📖 3 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een detective bent die een mysterie probeert op te lossen, maar je mag alleen een specifieke set aanwijzingen gebruiken. Je hebt een lang, ingewikkeld rapport van één getuige (laten we die "De Aanklager" noemen) en een tegenrapport van een andere ("De Verdediger"). Jouw taak is om één korte zin te vinden die het conflict tussen hen uitlegt. Deze zin moet het "middenpad" zijn: het moet waar zijn als de Aanklager gelijk heeft, en het moet onwaar zijn als de Verdediger gelijk heeft. Cruciaal is dat deze zin alleen woorden mag gebruiken die in beide rapporten voorkomen. Als de Aanklager over "katten" en "muizen" praat en de Verdefender over "honden" en "botten", mag jouw middenzin geen woorden als "katten" of "botten" bevatten; het kan alleen woorden gebruiken zoals "dieren" of "achtervolgen" als die woorden in beide verhalen voorkomen. In de wereld van de informatica wordt dit detectivegame de Craig Interpolation Property genoemd. Het is een superkracht die computers helpt te begrijpen hoe verschillende onderdelen van een systeem met elkaar samenhangen zonder in de war te raken door irrelevante details.

De specifieke detectivegame die dit artikel behandelt, betreft Propositional Dynamic Logic (PDL). Denk aan PDL als een taal voor het beschrijven van hoe computerprogramma's zich gedragen. Het is als een regelboek voor een videogame dat zegt: "Als je op 'A' drukt, dan 'B', dan spring je," of "Als je 'X' blijft indrukken, dan vlieg je uiteindelijk." Het lastige deel is het "uiteindelijk" of "blijf dit voor eeuwig doen" gedeelte, wat de logica zeer krachtig maakt maar ook erg moeilijk op te lossen. Decennialang hebben wiskundigen en informatici geprobeerd te bewijzen dat dit specifieke regelboek (PDL) de superkracht van interpolatie bezit. Drie verschillende teams probeerden het puzzelstuk op te lossen, maar hun oplossingen bleken gaten te bevatten, waardoor de vraag open bleef en frustrerend was.

Dit artikel lost het mysterie eindelijk op. De auteurs, een team van onderzoekers uit Duitsland en Nederland, hebben een gloednieuw, rigoureus bewijs geconstrueerd dat Propositional Dynamic Logic inderdaad de Craig Interpolation Property bezit. Ze hebben niet alleen gegokt; ze hebben een specifiek hulpmiddel gebouwd genaamd een "cyclic tableau system". Stel je dit systeem voor als een enorme, vertakkende boom waarbij je probeert een complexe logische puzzel op te splitsen in steeds kleinere stukjes. Normaal gesproken groeien deze bomen eeuwig door, maar de auteurs hebben een speciale "laadmechanisme" toegevoegd dat fungeert als een vangnet. Als de boom begint te cirkelen (wat gebeurt wanneer programma's acties herhalen), herkent dit mechanisme de lus en stopt het de groei, waardoor het bewijs eindig en beheersbaar blijft.

Met behulp van dit nieuwe boombouw-instrument hebben de auteurs aangetoond dat voor elke geldige logische bewering in PDL, je altijd die perfecte "middenzin" (de interpolant) kunt vinden die twee kanten van een argument verbindt met behulp van alleen hun gedeelde vocabulaire. Ze hebben niet alleen bewezen dat deze bestaat; ze hebben precies getoond hoe je deze kunt berekenen. Ze hebben zelfs een computerprogramma geschreven in een taal genaamd Haskell dat deze berekening voor je kan uitvoeren, en ze werken momenteel aan een tweede laag van bewijs met behulp van een digitale assistent genaamd "Lean" om te verifiëren dat hun wiskunde 100% correct is. Hoewel ze het hoofdraadsel hebben opgelost, geven ze toe dat sommige kleinere, gerelateerde vragen — zoals of dit werkt voor een vereenvoudigde versie van de logica zonder "test"-commando's — open blijven voor toekomstige detectives om op te lossen. Maar voor nu is het grote antwoord gegeven: PDL bezit de superkracht van interpolatie, en we weten nu precies hoe we het kunnen gebruiken.

Technische Samenvatting: Propositionele Dynamische Logica Bezit Craig-interpolatie

1. Het Probleem

Het artikel behandelt de langlopende open vraag of Propositionele Dynamische Logica (PDL) de Craig-interpolatie-eigenschap (CIP) bezit. CIP stelt dat voor elke geldige implicatie $\phi \to \psi$ er een interpolant $\theta$ bestaat waarvoor $\phi \to \theta$ en $\theta \to \psi$ geldig zijn, en $\theta$ alleen propositionele letters en atomaire programma's bevat die gemeenschappelijk zijn aan zowel $\phi$ als $\psi$ .

Hoewel PDL een goed bestudeerde modale logica is met gevestigde beslisbaarheid en volledigheidsresultaten, is de interpolatiestatus ervan decennialang onduidelijk gebleven. De literatuur bevat drie eerdere pogingen om interpolatie te bewijzen:

Leivant (1981): Claimde een bewijs, dat later door Kracht (1999) werd weerlegd vanwege onjuiste redenen, hoewel een werkelijke kloof in Leivants bewijs blijft bestaan.
Borzechowski (1988): Een masterscriptie (Diplomarbeit) die een bewijs claimde, welke weinig aandacht kreeg en door sommigen werd afgedaan als onverifieerbaar.
Kowalski (2002): Claimde een bewijs, dat werd weerlegd en in 2004 officieel werd ingetrokken.

De moeilijkheid ontstaat omdat PDL een modale fixpuntlogica is (vanwege de iteratie-operator $*$ ). Hoewel interpolatie is vastgesteld voor de volledige $\mu$ -calculus en de alternatie-vrije fragmenten via cyclische bewijssystemen, maken de specifieke beperkingen van PDL het uitdagend om te garanderen dat de oplossingen voor de fixpuntvergelijkingen die de interpolanten karakteriseren, binnen PDL zelf kunnen worden uitgedrukt, in plaats van de volledige expressieve kracht van de $\mu$ -calculus te vereisen.

2. Methodologie

De auteurs bieden een constructief bewijs gebaseerd op een cyclisch tableau-systeem en een adaptatie van de bewijs-theoretische methode van Maehara.

2.1. Een Cyclisch Tableau-systeem voor PDL

De auteurs definiëren een nieuw tableau-systeem voor PDL dat opereert op gesplitste sequenten (paren van verzamelingen formules). Belangrijke kenmerken zijn:

Lokale versus Modale Redenering: Het systeem maakt onderscheid tussen lokale regels (propositionele redenering en het ontvouwen van programma's binnen een enkele toestand) en modale regels (bewegen tussen toestanden in een Kripke-model).
Ontvouwingsmechanisme: In plaats van standaard reductieregels voor elk programmaconstructor, gebruikt het systeem een "loading"-mechanisme. Formules van de vorm $[\alpha]\psi$ (waarbij $\alpha$ niet-atomair is) worden uitgeplooid in een eindige verzameling sequenten op basis van "testprofielen". Deze verzameling, aangeduid als $\text{unfold}_\square(\alpha, \psi)$ , representeert de disjunctie van alle mogelijke executiepaden van $\alpha$ waar specifieke tests slagen of falen.
Afhandeling van Iteratie: Om oneindige lokale ontvouwing van formules zoals $[\alpha^*]\psi$ te voorkomen, elimineert het systeem geregenereerde voorkomens van de formule tijdens het ontvouwingsproces. Dit berust op de observatie dat $[\alpha^*]\psi$ een grootste fixpunt is.
Cyclische Bewijzen: Het systeem staat "repeats" toe (nodes met identieke labels als een voorouder).
- Loaded-path repeats: Een repeat waarbij het pad van de voorouder (companion) naar de huidige node volledig uit geladen nodes bestaat. Deze worden behanden als "succesvolle" bladeren (wat wijst op een lus die de formule voldoet).
- Free repeats: Een repeat waarbij het pad geladen nodes bevat. Deze worden behandeld als "mislukte" bladeren, wat duidt op een potentieel tegenmodel.
Terminatie: Het systeem garandeert eindigheid door af te dwingen dat alle free repeats en loaded-path repeats bladeren zijn, en door gebruik te maken van de Fischer-Ladner-closure om de verzameling formules te begrenzen.

2.2. Interpolatie via Quasi-tableaux en Fixpuntvergelijkingen

Om de interpolant te construeren, passen de auteurs de methode van Maehara aan voor de cyclische setting:

Clusters: Het tableau wordt beschouwd als een graaf met terugwaartse randen van repeats naar companions. De sterk samenhangende componenten (SCC's) van deze graaf worden "clusters" genoemd.
Quasi-tableaux: Voor een correcte cluster (een niet-singleton SCC) definiëren de auteurs een "quasi-tableau". Deze structuur wordt gebruikt om een systeem van vergelijkingen op te zetten die de interpolant karakteriseren.
Pre-interpolanten: De methode definieert "pre-interpolanten" voor nodes in het quasi-tableau via blad-naar-wortel inductie.
- Bij exit nodes (bladeren die geen deel uitmaken van de cluster) is de pre-interpolant de interpolant van de exit node (verondersteld te bestaan bij inductie).
- Bij repeat leaves is de pre-interpolant een interne propositionele variabele $q_x$ .
- Bij companion nodes wordt de pre-interpolant gedefinieerd als de oplossing van een fixpuntvergelijking. Specifiek, als een companion $x$ een kind $y$ heeft met pre-interpolant $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$ , dan is de pre-interpolant voor $x$ gedefinieerd als $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$ .
Oplossen in PDL: Het cruciale inzicht is dat deze specifieke constructie ervoor zorgt dat de oplossingen van de fixpuntvergelijkingen binnen de taal van PDL blijven. Het gebruik van de iteratie-operator $*$ in de definitie van $\iota_x$ lost de vergelijking $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ effectief op binnen PDL.
Finale Interpolant: De interpolant voor de wortel van de cluster wordt verkregen door de interne variabelen in de pre-interpolant van de wortel te vervangen door de overeenkomstige regio-formules (disjuncties van de linkerzijden van de gesplitste sequenten).

3. Belangrijkste Bijdragen en Resultaten

Bewijs van CIP voor PDL: Het artikel stelt vast dat PDL de Craig-interpolatie-eigenschap bezit.
Beth Definability: Als een gevolg van het artikel bewijst het dat PDL de Beth-definabiliteitseigenschap bezit (aangezien CIP Beth-definabiliteit impliceert in aanwezigheid van een deductiestelling).
Constructief Algoritme: Het bewijs is constructief. De auteurs bieden een duidelijk algoritme om interpolanten te berekenen vanuit een gesloten tableau.
Formele Verificatie: De auteurs hebben het bewijs gedeeltelijk geformaliseerd in de interactieve theorem prover Lean 4. Op het moment van schrijven van het artikel zijn de Soundness en Completeness stellingen, samen met verschillende ondersteunende lemma's, geverifieerd.
Implementatie: Een Haskell-implementatie van het tableau-systeem en de interpolant-constructie wordt geleverd, beschikbaar via een webinterface.

4. Betekenis en Claims

Het artikel beweert een puzzel in de literatuur over de interpolatiestatus van PDL op te lossen door het eerste geverifieerde bewijs te leveren dat de hiaten in eerdere pogingen overbrugt.

Resolutie van Historische Problemen: De auteurs adresseren expliciet de geschiedenis van mislukte pogingen, waarbij zij opmerken dat hun benadering bouwt op de kernideeën van Borzechowski (1988), maar de behandeling van cyclische bewijzen en de constructie van interpolanten binnen de taal van PDL rigoureus formaliseert.
Methodologische Nieuwheid: Het artikel benadrukt dat hoewel Maehara's methode standaard is voor niet-cyclische bewijzen, het toepassen ervan op cyclische bewijzen (fixpuntlogica's) het oplossen van fixpuntvergelijkingen vereist. De auteurs demonstreren dat voor PDL deze oplossingen met de eigen iteratie-operator van de logica kunnen worden uitgedrukt, een niet-triviaal resultaat dat PDL onderscheidt van andere fragmenten waar dergelijke oplossingen de volledige $\mu$ -calculus zouden kunnen vereisen.
Openstaande Vragen: De auteurs merken bescheiden op dat hun methode steunt op de aanwezigheid van test-programma's ( $\tau?$ ). Het blijft daarom een open vraag of het test-vrije fragment van PDL interpolatie bezit, aangezien hun constructie over het algemeen interpolanten oplevert die tests bevatten, zelfs wanneer de input test-vrij is. Zij laten ook de uitbreiding van hun methode naar andere PDL-varianten (bijv. met converse of intersectie) en de implicaties voor Kleene Algebra met Tests (KAT) open.

Samenvattend biedt het artikel een definitief, constructief bewijs van Craig-interpolatie voor PDL met behulp van een nieuw cyclisch tableau-systeem en een gespecialiseerde fixpunt-oplossingstechniek voor interpolanten, ondersteund door zowel een Haskell-implementatie als een gedeeltelijke formele verificatie in Lean.