Partially Finite Model Reasoning in Description Logics Extended Version

1. Enunciato del Problema

Il lavoro affronta il divario tra la ragionamento su modelli infiniti (standard nelle Logiche Descrittive, dove i modelli possono essere arbitrariamente grandi) e la ragionamento su modelli finiti (standard nei database, dove i domini sono finiti). Mentre molte Logiche Descrittive (DL) esibiscono la finite controllability (dove l'implicazione delle query è identica per modelli finiti e infiniti), altre, come $\mathcal{S}$ (un'estensione di $\mathcal{ALC}$ con ruoli transitivi), non lo fanno. In queste logiche, una query potrebbe essere implicata in tutti i modelli finiti ma non in quelli infiniti, o viceversa.

Gli autori introducono il Ragionamento su Modelli Parzialmente Finiti. In questa modalità ibrida:

• Viene fornita una Base di Conoscenza (KB) insieme a un concetto distinto $F$.
• Il compito di ragionamento considera solo modelli in cui l'interpretazione di $F$ è un insieme finito di individui.
• Il resto del modello (elementi non in $F$) può essere infinito.
• Obiettivo: Decidere se una Query Coniuntiva (CQ) $Q$ è implicata dalla KB sotto il vincolo che $F$ sia finito (denotato $K \models_F Q$).

Questo quadro generalizza sia l'implicazione standard (dove nessun concetto è vincolato) sia l'implicazione finita (dove l'intero dominio è vincolato). Serve anche come fondamento teorico per il contenimento di query con predicati chiusi, dove certi predicati sono assunti avere estensioni finite.

2. Metodologia

Gli autori sviluppano una tecnica di dimostrazione sofisticata per decidere l'implicazione parzialmente finita per la logica $\mathcal{S}$. La metodologia coinvolge diversi passaggi chiave:

A. Quasi-Svolgimento (Quasi-Unravelling)

Per gestire modelli infiniti mantenendo la parte "finita" ($F$) gestibile, gli autori introducono il quasi-svolgimento.

• A differenza dello svolgimento standard (che crea un albero duplicando ogni nodo), il quasi-svolgimento crea una struttura simile a un albero in cui gli elementi critici (quelli in $F$) non sono duplicati.
• Solo gli elementi non critici vengono duplicati lungo i percorsi. Questo garantisce che la struttura risultante abbia un insieme finito di nodi critici, preservando la proprietà "parzialmente finita" mentre permette al resto del modello di essere simile a un albero per un'analisi più agevole.

B. Interpretazioni Elementari

Gli autori definiscono una classe di strutture finite chiamate interpretazioni elementari per servire come rappresentazioni finite di potenziali controesempi. Queste sono costruite gerarchicamente:

1. Singoli/Cicli/Cluster Critici: Blocchi costitutivi di base.
2. Alberi di Loop: Alberi formati attaccando alberi di loop a singoli o cicli (simili a cactus).
3. Interpretazioni Elementari: Alberi costruiti attaccando alberi di loop e cluster critici.
   L'intuizione fondamentale è che qualsiasi controesempio può essere trasformato in un'interpretazione elementare tramite quasi-svolgimento senza perdere la proprietà di essere un controesempio.

C. Bloccaggio Colorato e Quozienti

Per gestire ruoli transitivi multipli e garantire l'esistenza di un controesempio finito con le proprietà richieste, il lavoro adatta il Teorema del Bloccaggio Colorato.

• Definiscono una colorazione $k$-sparsa degli elementi critici.
• Utilizzando una relazione di equivalenza basata sui $k$-vicinati, costruiscono un'interpretazione quoziente.
• Dimostrano che se una query non è soddisfatta nel modello infinito originale, non è soddisfatta nemmeno nel quoziente (che è parzialmente finito), a condizione che la colorazione sia sufficientemente sparsa.

D. Il "Blow-Up" e la Decidibilità

Per rendere il problema decidibile, gli autori sostituiscono la condizione "il quasi-svolgimento non soddisfa $Q$" con una condizione verificabile su una versione "gonfiata" (blown-up) dell'interpretazione elementare ($G_n$).

• "Gonfiano" i cicli nell'interpretazione elementare fino a una lunghezza di $2n+1$ (dove $n$ è il numero di variabili nella query).
• Dimostrano che verificare se la struttura gonfiata $G_n$ soddisfa la query è equivalente a verificare il quasi-svolgimento per query di dimensione $n$.
• Questo permette di utilizzare una procedura di eliminazione dei tipi (simile agli approcci basati su automi) per cercare un testimone (un controesempio) all'interno di uno spazio di ricerca doppiamente esponenziale.

3. Contributi Chiave

1. Formalizzazione del Ragionamento Parzialmente Finito: Il lavoro avvia lo studio sistematico del ragionamento in cui solo parti specifiche di un modello sono vincolate a essere finite.
2. Risultato sulla Complessità per $\mathcal{S}$: Gli autori dimostrano che l'Implicazione di Query Parzialmente Finita per $\mathcal{S}$ è 2-ExpTime-completa.
   • Questo corrisponde alla complessità sia dell'implicazione infinita standard sia dell'implicazione finita per $\mathcal{S}$, mostrando che la modalità ibrida non aumenta la complessità computazionale.
3. Tecniche di Dimostrazione Innovative: La soluzione coinvolge una "chirurgia su modelli infiniti", combinando quasi-svolgimento, interpretazioni elementari e bloccaggio colorato in un modo che va oltre la semplice combinazione di argomenti per i casi finito e infinito.
4. Applicazione ai Predicati Chiusi: Il lavoro dimostra che il contenimento di query in presenza di predicati chiusi può essere ridotto all'implicazione parzialmente finita. Questo fornisce un nuovo limite superiore di complessità per il problema dei predicati chiusi in DL espressive.

4. Risultati

• Teorema Principale (Teorema 16): L'implicazione parzialmente finita di query coniuntive per la logica $\mathcal{S}$ è 2-ExpTime-completa.
• Caratterizzazione del Testimone: Se una KB non implica parzialmente finitamente una query, esiste un'interpretazione "elementare a pezzi" di dimensione limitata (esponenziale rispetto alla dimensione della KB) il cui quasi-svolgimento funge da controesempio.
• Riduzione: Il contenimento di query con predicati chiusi è risolvibile in Tempo Polinomiale Non Deterministico (NP) dato un oracolo per l'implicazione parzialmente finita.

5. Significato

• Colmare il Divario tra Teoria e Pratica: Il lavoro colma il divario tra la ricchezza teorica dei modelli infiniti (necessaria per logiche espressive) e i vincoli pratici dei domini finiti (necessari per applicazioni database).
• Gestione dei Predicati Chiusi: I predicati chiusi (dove l'estensione di un concetto è nota e finita) sono cruciali per l'integrazione di database e la risposta alle query mediate da ontologie. Questo lavoro fornisce una fondazione rigorosa basata sulla teoria della complessità per il ragionamento con essi in logiche espressive come $\mathcal{S}$.
• Insight sulla Scalabilità: Il risultato sulla complessità (2-ExpTime) suggerisce che, sebbene il problema sia difficile, non è indecidibile, e i limiti superiori si allineano con sistemi esistenti (come SUMA) che utilizzano strategie di materializzazione parziale.
• Direzioni Future: Gli autori suggeriscono di estendere queste tecniche ad altre logiche prive di finite controllability (ad esempio $\mathcal{ALCIF}$) e ad altri compiti di ragionamento come il contenimento e l'enumerazione delle query.

In sintesi, il lavoro stabilisce con successo che il ragionamento con vincoli "parzialmente finiti" è computazionalmente fattibile e fornisce la necessaria macchina teorico-modelistica per gestire la divergenza tra modelli finiti e infiniti nelle Logiche Descrittive espressive.