A New Tractable Description Logic under Categorical Semantics

1. Il Problema

Le ontologie biomediche (come SNOMED CT, GO, ICD) contengono una vasta quantità di conoscenza negativa, espressa tramite etichette come "mancanza di parte" (lacks part), "assenza di" (absence of) o "controindicazione".

• Limitazione delle Logiche Tracciabili: Le logiche descrittive (DL) tracciabili, come la famiglia EL (che supporta congiunzione, restrizione esistenziale e inclusione di concetti), sono ampiamente utilizzate per la loro efficienza computazionale (tempo polinomiale). Tuttavia, per mantenere la tracciabilità, queste logiche devono rinunciare alla negazione.
• Il Paradosso della Negazione: Aggiungere la negazione classica a EL rende la logica intrattabile (complessità esponenziale o EXPTIME-completa). Questo accade perché la negazione introduce implicitamente la disgiunzione ($\sqcup$) e la restrizione universale ($\forall$). Le interazioni tra questi costruttori (in particolare tra restrizione esistenziale $\exists$ e universale $\forall$, e tra congiunzione $\sqcap$ e disgiunzione $\sqcup$) generano un'esplosione combinatoria durante il ragionamento.
• Inadeguatezza delle Etichette: Rappresentare la negazione tramite semplici etichette (es. lacks_part invece di ¬has_part) impedisce al reasoner di interpretare semanticamente la relazione logica tra i concetti, limitando l'inferenza.

L'obiettivo è creare una nuova logica che supporti la conoscenza negativa mantenendo la tracciabilità.

2. Metodologia: Semantica Categorica

Gli autori propongono un approccio basato sulla Teoria delle Categorie per ridefinire la semantica delle logiche descrittive, abbandonando la semantica insiemistica classica (basata su appartenenza a insiemi $\in$).

• Dagli Insiemi alle Frecce: Invece di definire i concetti come sottoinsiemi di un dominio, i concetti sono oggetti in una categoria e le relazioni di inclusione sono frecce ($\to$).
• Decomposizione delle Proprietà: La semantica categorica permette di scomporre i costruttori logici in una serie di proprietà indipendenti (definite tramite diagrammi e proprietà universali come prodotti, coproducti e adjunzioni).
  • Ad esempio, la congiunzione è definita da proprietà di decomposizione e composizione.
  • La disgiunzione e la restrizione universale sono definite tramite proprietà di massimo/minimo e adjunzioni.
• Identificazione delle Cause di Intrattabilità: Analizzando le proprietà categoriche, gli autori identificano che l'intrattabilità non deriva dai costruttori in sé, ma da specifiche interazioni tra di essi:
  1. Interazione $\exists$ e $\forall$: La proprietà che permette di derivare $\exists R.(C \sqcap D)$ da $\exists R.C \sqcap \forall R.D$ (che porta a un'esplosione esponenziale di restrizioni esistenziali composte).
  2. Distributività di $\sqcap$ su $\sqcup$: La proprietà che permette di distribuire la congiunzione sulla disgiunzione, generando un numero esponenziale di casi nel ragionamento (regola del $\sqcup$ nei tableaux).

3. Contributi Chiave

A. Semantica Categorica per SH

Gli autori definiscono la semantica categorica completa per la logica SH (che include negazione, disgiunzione, restrizione universale, ruoli transitivi e inclusione di ruoli). Dimostrano che questa semantica è equivalente a quella insiemistica: un'ontologia è inconsistente nella semantica categorica se e solo se lo è in quella insiemistica.

B. Introduzione di $EL^\rightarrow$

Sfruttando l'indipendenza delle proprietà categoriche, gli autori propongono una nuova logica, $EL^\rightarrow$, ottenuta "indebolendo" la semantica di SH rimuovendo o modificando le proprietà responsabili dell'intrattabilità:

1. Rimozione della Distributività: Si elimina la proprietà $P^\sqcap_\sqcup$ che permette di derivare $(C \sqcap D) \sqcup (C \sqcap E)$ da $C \sqcap (D \sqcup E)$.
2. Indebolimento dell'Interazione $\exists/\forall$: Si sostituiscono le proprietà $P^\forall_\exists$ e P^\forall_\exists^\circ con versioni indebolite ($\bar{P}^\forall_\exists$, \bar{P}^\forall_\exists^\circ). Queste nuove proprietà permettono di rilevare solo la disgiunzione binaria (es. $C \sqcap D \sqsubseteq \bot$) ma non quella $n$-aria ($C \sqcap D_1 \sqcap \dots \sqcap D_n \sqsubseteq \bot$) quando $n > 2$.
3. Negazione Indebolita ($\bar{\neg}$): Poiché la negazione è definita tramite disgiunzione e congiunzione, anche essa viene indebolita di conseguenza.

C. Tracciabilità e Algoritmo

• Viene definito un insieme di regole di inferenza categorica per $EL^\rightarrow$.
• Teorema di Complessità: Viene dimostrato che il numero di oggetti e frecce generati durante il ragionamento in $EL^\rightarrow$ è limitato da una funzione polinomiale rispetto alla dimensione dell'ontologia. Di conseguenza, il controllo di consistenza è tracciabile (P-time).
• Espressività: $EL^\rightarrow$ è più espressiva di $EL^\circ_\bot$ (EL con concetto vuoto e ruoli transitivi) perché permette di rappresentare la negazione e la disgiunzione in modo controllato, pur essendo meno espressiva di SH completa.

4. Risultati e Analisi

• Correttezza: È stato provato che $EL^\rightarrow$ è un'estensione corretta di $EL^\circ_\bot$. Se un'ontologia è inconsistente in SH, lo è anche in $EL^\rightarrow$ (Corollario 3). Tuttavia, il viceversa non è sempre vero: $EL^\rightarrow$ potrebbe non rilevare inconsistenze che dipendono da interazioni $n$-arie complesse ($n \ge 3$).
• Rilevanza Biomedica: Gli autori sostengono che nelle ontologie biomediche reali (SNOMED CT, MONDO, ecc.), le inconsistenze che richiedono la rilevazione di disgiunzioni $n$-arie ($n \ge 3$) sono estremamente rare o inesistenti. La maggior parte delle conoscenze negative può essere catturata efficacemente rilevando solo la disgiunzione binaria (es. un paziente non può avere sia Penicillina che allergia alla Penicillina).
• Indipendenza: I costruttori indeboliti ($\bar{\forall}, \bar{\sqcup}, \bar{\neg}$) sono indipendenti dagli altri costruttori, permettendo di costruire la logica in modo modulare.

5. Significato e Implicazioni

• Nuovo Paradigma di Ragionamento: Il lavoro dimostra che la teoria delle categorie non è solo un formalismo astratto, ma uno strumento pratico per "ingegnerizzare" la complessità computazionale delle logiche. Isolando le proprietà semantiche specifiche che causano l'esplosione esponenziale, è possibile rimuoverle selettivamente senza perdere l'utilità pratica per domini specifici.
• Gestione della Negazione in EL: Fornisce una soluzione teorica e pratica per integrare la conoscenza negativa nelle ontologie biomediche mantenendo l'efficienza di EL, superando la necessità di usare etichette non semantiche.
• Flessibilità Semantica: La semantica categorica offre una visione più modulare della logica rispetto alla semantica insiemistica, dove le interazioni sono "nascoste". Questo permette di progettare nuove logiche con complessità di ragionamento personalizzate.
• Prospettive Future: Gli autori pianificano l'implementazione di un reasoner chiamato Ela basato su queste regole, da confrontare con reasoner basati su semantica insiemistica (come Konclude) su grandi ontologie mediche. Si prevede che Ela possa restituire più istanze (essendo meno restrittivo) mantenendo tempi di risposta rapidi, con una validazione da parte di esperti del dominio medico.

In sintesi, il paper propone una via innovativa per bilanciare espressività e tracciabilità, utilizzando la teoria delle categorie per sminuire le interazioni logiche che causano intrattabilità, rendendo possibile l'uso di negazione in contesti biomedici critici per le prestazioni.