Computation and Size of Interpolants for Hybrid Modal Logics

Technische Samenvatting: Berekening en Grootte van Interpolanten voor Hybride Modale Logica's

Probleemstelling
Het artikel behandelt de computationele complexiteit en constructie van Craig-interpolanten in hybride modale logica's (specifiek $H$, $H@$, $H@,U$, en hun gegradeerde uitbreidingen $GHL$). Hoewel recent onderzoek de complexiteit van het beslissen over het bestaan van interpolanten in logica's die het Craig-interpolatie-eigenschap (CIP) missen, heeft vastgesteld, blijft de constructie van dergelijke interpolanten een open uitdaging. Bestaande beslissingsprocedures zijn niet-constructief; ze vertrouwen op compactheidsargumenten (bijvoorbeeld de gezamenlijke consistentie van Robinson) in plaats van expliciete formules te leveren. Bijgevolg zijn er voor deze logica's geen betekenisvolle bovengrenzen voor de grootte van interpolanten bekend.

Dit probleem is bijzonder acuut voor hybride modale logica's (en beschrijvingslogica's met nomina's) omdat:

1. CIP niet kan worden hersteld door logische connectieven toe te voegen zonder de beslisbaarheid op te offeren.
2. Interpolanten in deze logica's kritieke toepassingen hebben in kennisrepresentatie, zoals het verklaren van schendingen van modulariteit, het scheiden van positieve en negatieve data-voorbeelden, en het leveren van definitieve beschrijvingen.

Methodologie
De auteurs introduceren een nieuwe constructieve techniek genaamd hypermozaïek-eliminatie. Deze methode breidt de standaard "type-eliminatie"-procedure uit die wordt gebruikt voor satisfiability in modale logica's, en de "mozaïek"-benadering die wordt gebruikt voor het beslissen van het bestaan van interpolanten in niet-CIP-logica's.

1. Van Types naar Mozaïeken naar Hypermozaïeken:

   • Standaard type-eliminatie werkt met paren van types.
   • Mozaïek-eliminatie (gebruikt voor beslissingsprocedures) werkt met paren van verzamelingen van types om niet-gedeelde nomina's te behandelen.
   • De auteurs betogen dat mozaïek-eliminatie te lokaal is om interpolanten te berekenen, omdat het geen globale interacties tussen verschillende "nominaalgevallen" (scenario's over hoe nomina's worden geïnterpreteerd) kan vastleggen.
   • Om dit te overwinnen, definiëren zij hypermozaïeken: verzamelingen van mozaïeken die gelijktijdig moeten worden gerealiseerd in bisimulaire modellen. Deze structuur stelt het algoritme in staat om globale beperkingen over verschillende nominaalinterpretaties bij te houden.

2. Eliminatieprocedure:

   • De procedure begint met een verzameling van alle $\sigma$-consistente en nominaal-schone hypermozaïeken.
   • Het elimineert iteratief hypermozaïeken die een "getuige" missen. Een getuige voor een hypermozaïek $H$ is een uitbreidend hypermozaïek $H'$ dat specifieke coherentievoorwaarden voldoet (bijvoorbeeld voor gegradeerde logica's moeten kwantitatieve beperkingen op opvolgers worden voldaan via tel-functies).
   • De procedure stabiliseert bij een verzameling $Z^*$ van realiseerbare hypermozaïeken. Als het initiële hypermozaïek dat de invoerformules bevat, wordt geëlimineerd, zijn de formules niet gezamenlijk consistent, en bestaat er een interpolant.

3. Constructieve Scheiderconstructie:

   • Het artikel construeert hyper-scheiders inductief naast het eliminatieproces.
   • Een hyper-scheider bestaat uit een "casusonderscheid" (uitputtende scenario's voor nominaal-types) en functies die types afbeelden op formules.
   • In elke eliminatieronde wordt het casusonderscheid verfijnd om de "ster-types" (lokale omgevingen) van de geëlimineerde hypermozaïeken vast te leggen.
   • Deze constructie transformeert het niet-constructieve bestaanbewijs in een expliciet algoritme dat de interpolant (of scheider) genereert.

Belangrijkste Bijdragen en Resultaten

• Bovengrenzen voor Grootte en Complexiteit:
  Het primaire resultaat (Stelling 1) stelt dat voor elke logica $L \in HL \cup GHL$, als er een Craig-interpolant bestaat voor $\phi \to \psi$, deze kan worden geconstrueerd in viervoudig exponentiële tijd, en dat de resulterende interpolant een grootte heeft van viervoudig exponentieel in de grootte van de invoerformules.

  • Opmerking: Het bewijs vertrouwt op het feit dat hoewel er drievoudig exponentieel veel hypermozaïeken zijn, de eliminatieprocedure stabiliseert na maximaal tweevoudig exponentieel veel rondes vanwege de monotonie van getuigen.

• Ondergrenzen:
  Het artikel levert een drievoudig exponentiële ondergrens voor de grootte van Craig-interpolanten (en tweevoudig exponentieel voor DAG-grootte) voor logica's met de universele modus ($H@,U$ en $G@,U$). Dit toont aan dat interpolanten in hybride logica's inherent groter zijn dan in standaard modale logica (waar ze doorgaans exponentieel zijn).

• Onbeslisbaarheid van Uniforme Interpolanten:
  In schril contrast tot standaard modale en intuïtionistische logica's (waar uniforme interpolanten altijd bestaan en vaak construeerbaar zijn), bewijst het artikel (Stelling 3) dat het bestaan van uniforme interpolanten onbeslisbaar is voor elke logica die $H$ bevat en die in Eerste Orde Logica (FO) is opgenomen. Dit wordt aangetoond via een reductie vanuit de onbeslisbaarheid van het definiëren van eindige lineaire ordeningen van even lengte in FO.

• Gegradeerde Uitbreidingen:
  De methodologie wordt succesvol uitgebreid naar gegradeerde hybride logica's ($GHL$), die gekwalificeerde aantalbeperkingen bevatten. De auteurs passen de definitie van een getuige aan om tel-functies op te nemen en tonen aan dat de viervoudig exponentiële bovengrens ook voor deze logica's geldt.

Betekenis en Claims
De auteurs claimen de eerste elementaire bovengrenzen te leveren voor het construeren van Craig-interpolanten in een familie van beslisbare logica's waar CIP faalt en niet eenvoudig kan worden gerepareerd.

• Constructief versus Niet-Constructief: Het werk overbrugt de kloof tussen het weten dat een interpolant bestaat (beslisbaarheid) en hoe deze te berekenen. Eerdere methoden waren niet-constructief; dit artikel levert een expliciet algoritme.
• Robuustheid: De constructiemethode blijkt robuust onder taalbeperkingen (bijvoorbeeld het berekenen van interpolanten in een zwakkere sub-taal) en kan worden aangepast om standaard beperkingen zoals transitiviteit en reflexiviteit te behandelen.
• Beperkingen: Het artikel erkent dat de exacte complexiteitskloof tussen de viervoudig exponentiële bovengrens en de drievoudig exponentiële ondergrens open blijft. Bovendien blijft de uitbreiding naar inverse relaties of de hybride $\mu$-calculus een open vraag, aangezien het bestaan van interpolanten in die specifieke uitbreidingen onbeslisbaar kan zijn of niet-elementaire grenzen vereist.

Kortom, het artikel stelt vast dat hoewel interpolanten in hybride modale logica's computationeel duur zijn (viervoudig exponentieel), ze effectief berekenbaar zijn, en zo een constructieve basis bieden voor toepassingen in kennisrepresentatie die eerder vertrouwden op niet-constructieve bestaanbewijzen.