Computation and Size of Interpolants for Hybrid Modal Logics

Sintesi Tecnica: Computazione e Dimensione degli Interpolanti per Logiche Modali Ibride

Enunciato del Problema
Il lavoro affronta la complessità computazionale e la costruzione di interpolanti di Craig nelle logiche modali ibride (in particolare $H$, $H@$, $H@,U$ e le loro estensioni graduate $GHL$). Sebbene ricerche recenti abbiano stabilito la complessità del decidere l'esistenza di interpolanti in logiche prive della Proprietà di Interpolazione di Craig (CIP), la costruzione di tali interpolanti rimane una sfida aperta. Le procedure decisionali esistenti sono non costruttive, basandosi su argomenti di compattezza (ad esempio, la coerenza congiunta di Robinson) piuttosto che fornire formule esplicite. Di conseguenza, non sono noti limiti superiori significativi sulla dimensione degli interpolanti per queste logiche.

Questo problema è particolarmente acuto per le logiche modali ibride (e le logiche descrittive con nomi) perché:

1. La CIP non può essere ripristinata aggiungendo connettivi logici senza sacrificare la decidibilità.
2. Gli interpolanti in queste logiche hanno applicazioni critiche nella rappresentazione della conoscenza, come spiegare violazioni della modularità, separare esempi di dati positivi e negativi e fornire descrizioni definite.

Metodologia
Gli autori introducono una nuova tecnica costruttiva chiamata eliminazione di iper-mosaico. Questo metodo estende la procedura standard di "eliminazione dei tipi" utilizzata per la soddisfacibilità nelle logiche modali e l'approccio "mosaico" utilizzato per decidere l'esistenza di interpolanti nelle logiche senza CIP.

1. Dai Tipi ai Mosaici agli Iper-mosaici:

   • L'eliminazione standard dei tipi lavora con coppie di tipi.
   • L'eliminazione dei mosaici (utilizzata per le procedure decisionali) lavora con coppie di insiemi di tipi per gestire i nomi non condivisi.
   • Gli autori sostengono che l'eliminazione dei mosaici è troppo locale per calcolare gli interpolanti perché non può catturare le interazioni globali tra diversi "casi di nomi" (scenari riguardanti come i nomi sono interpretati).
   • Per superare questo limite, definiscono gli iper-mosaici: insiemi di mosaici che devono essere realizzati simultaneamente in modelli bisimili. Questa struttura permette all'algoritmo di tracciare vincoli globali attraverso diverse interpretazioni dei nomi.

2. Procedura di Eliminazione:

   • La procedura inizia con un insieme di tutti gli iper-mosaici $\sigma$-consistenti e puliti dai nomi.
   • Elimina iterativamente gli iper-mosaici privi di un "testimone". Un testimone per un iper-mosaico $H$ è un iper-mosaico estendente $H'$ che soddisfa condizioni specifiche di coerenza (ad esempio, per le logiche graduate, i vincoli quantitativi sui successori devono essere soddisfatti tramite funzioni di conteggio).
   • La procedura si stabilizza su un insieme $Z^*$ di iper-mosaici realizzabili. Se l'iper-mosaico iniziale contenente le formule di input viene eliminato, le formule non sono congiuntamente consistenti e un interpolante esiste.

3. Costruzione Costruttiva del Separatore:

   • Il lavoro costruisce iper-separatori in modo induttivo insieme al processo di eliminazione.
   • Un iper-separatore consiste in una "distinzione di casi" (scenari esaustivi per i tipi di nomi) e funzioni che mappano i tipi su formule.
   • In ogni round di eliminazione, la distinzione di casi viene raffinata per catturare i "tipi-stella" (intorni locali) degli iper-mosaici eliminati.
   • Questa costruzione trasforma la prova di esistenza non costruttiva in un algoritmo esplicito che genera l'interpolante (o il separatore).

Contributi e Risultati Chiave

• Limiti Superiori su Dimensione e Complessità:
  Il risultato principale (Teorema 1) stabilisce che per qualsiasi logica $L \in HL \cup GHL$, se un interpolante di Craig esiste per $\phi \to \psi$, può essere costruito in tempo esponenziale quadruplo, e l'interpolante risultante ha una dimensione di esponenziale quadruplo rispetto alla dimensione delle formule di input.

  • Nota: La prova si basa sul fatto che, sebbene vi siano esponenziali tripli di iper-mosaici, la procedura di eliminazione si stabilizzi dopo al massimo esponenziali doppi di round a causa della monotonia dei testimoni.

• Limiti Inferiori:
  Il lavoro fornisce un limite inferiore esponenziale triplo sulla dimensione degli interpolanti di Craig (e esponenziale doppio per la dimensione DAG) per le logiche con il modale universale ($H@,U$ e $G@,U$). Ciò dimostra che gli interpolanti nelle logiche ibride sono intrinsecamente più grandi rispetto alla logica modale standard (dove sono tipicamente esponenziali).

• Indecidibilità degli Interpolanti Uniformi:
  In netto contrasto con le logiche modali standard e intuizioniste (dove gli interpolanti uniformi esistono sempre e sono spesso costruibili), il lavoro dimostra (Teorema 3) che l'esistenza di interpolanti uniformi è indecidibile per qualsiasi logica contenente $H$ e contenuta nella Logica del Primo Ordine (FO). Ciò è mostrato tramite una riduzione dall'indecidibilità della definizione di ordini lineari finiti di lunghezza pari in FO.

• Estensioni Graduate:
  La metodologia è estesa con successo alle logiche ibride graduate ($GHL$), che includono restrizioni numeriche qualificate. Gli autori adattano la definizione di testimone per includere funzioni di conteggio e dimostrano che il limite superiore esponenziale quadruplo vale anche per queste logiche.

Significato e Affermazioni
Gli autori affermano di fornire i primi limiti superiori elementari per la costruzione di interpolanti di Craig in una famiglia di logiche decidibili in cui la CIP fallisce e non può essere facilmente riparata.

• Costruttivo vs Non Costruttivo: Il lavoro colma il divario tra sapere che un interpolante esiste (decidibilità) e come calcolarlo. I metodi precedenti erano non costruttivi; questo lavoro fornisce un algoritmo esplicito.
• Robustezza: Il metodo di costruzione si dimostra robusto sotto restrizioni linguistiche (ad esempio, calcolare interpolanti in un sotto-linguaggio più debole) e può essere adattato per gestire vincoli standard come transitività e riflessività.
• Limitazioni: Il lavoro riconosce che il divario di complessità esatto tra il limite superiore esponenziale quadruplo e il limite inferiore esponenziale triplo rimane aperto. Inoltre, l'estensione alle relazioni inverse o al calcolo $\mu$ ibrido rimane una questione aperta, poiché l'esistenza di interpolanti in quelle specifiche estensioni potrebbe essere indecidibile o richiedere limiti non elementari.

In sintesi, il lavoro stabilisce che, sebbene gli interpolanti nelle logiche modali ibride siano computazionalmente costosi (esponenziale quadruplo), sono effettivamente calcolabili, offrendo una base costruttiva per applicazioni nella rappresentazione della conoscenza che in precedenza si affidavano a prove di esistenza non costruttive.