A New Tractable Description Logic under Categorical Semantics

Probleemstelling

Biomedische ontologieën (zoals SNOMED-CT en GO) bevatten talrijke concepten en rollen die negatieve kennis uitdrukken, zoals "ontbreekt deel" (lacks part) of "afwezigheid van" (absence of). In de huidige praktijk worden deze vaak gemodelleerd als losse labels in plaats van logische constructoren. Dit belemmert redeneersystemen om deze labels te interpreteren als de negatie van een bestaande relatie (bijv. de negatie van has part).

Het toevoegen van volledige negatie aan de tractabele Beschrijvingslogica (DL) EL (die alleen conjunctie, existentiële restrictie en concept-inclusie toestaat) maakt de logica ontractabel (EXPTIME-compleet). Dit komt omdat negatie impliciet disjunctie ($\sqcup$) en universele restrictie ($\forall$) introduceert. De interactie tussen deze constructoren leidt tot een exponentiële explosie in de redeneeralgoritmen. Bestaande pogingen om tractabiliteit te behouden terwijl negatie wordt toegevoegd, zijn beperkt omdat ze vastzitten aan de gebruikelijke verzamelingstheoretische semantiek (set-theoretic semantics), waar negatie en disjunctie onlosmakelijk verbonden zijn met de complexiteit.

Methodologie: Categorie-theoretische Semantiek

De auteurs introduceren een nieuwe aanpak door de semantiek van DL's te herschrijven met behulp van categorie-theorie. In plaats van concepten te interpreteren als verzamelingen van individuen (met element-relaties $\in$), worden concepten geïnterpreteerd als objecten in een categorie en relaties als pijlen (arrows).

1. Decompositie van Semantiek: In de categorie-theoretische benadering wordt de betekenis van een logische constructor niet gedefinieerd door één enkele operatie (zoals unie of complement), maar door een verzameling onafhankelijke categorische eigenschappen (pijlen en hun composities).
2. Identificatie van Ontractabiliteit: De auteurs analyseren welke specifieke interacties tussen constructoren verantwoordelijk zijn voor de ontractabiliteit. Ze identificeren twee kritieke eigenschappen die leiden tot exponentiële groei:
   • Interactie tussen $\exists$ en $\forall$: De eigenschap die stelt dat $\exists R.C \sqcap \forall R.D \sqsubseteq \exists R.(C \sqcap D)$. Dit leidt tot het creëren van nieuwe, complexe existentiële restricties bij het redeneren.
   • Distributiviteit van $\sqcap$ over $\sqcup$: De eigenschap $A \sqcap (B \sqcup C) \sqsubseteq (A \sqcap B) \sqcup (A \sqcap C)$. Dit veroorzaakt een exponentieel aantal takken in redeneerprocedures (tableau-methoden).
3. Verzwakking van Semantiek: Om tractabiliteit te behouden, worden deze specifieke interactie-eigenschappen verwijderd of verzwakt uit de verzameling van categorische axioma's.
   • De universele restrictie ($\forall$) wordt vervangen door een verzwakte versie ($\bar{\forall}$) die alleen binaire disjunctiviteit controleert (bijv. $C \sqcap D \sqsubseteq \bot$) in plaats van $n$-voudige disjunctiviteit.
   • De disjunctie ($\sqcup$) wordt verzwakt tot $\bar{\sqcup}$ door de distributiviteit over conjunctie te verwijderen.
   • Negatie ($\neg$) wordt hierdoor ook verzwakt tot $\bar{\neg}$, maar behoudt wel de capaciteit om negatieve kennis in biomedische contexten te modelleren.

Belangrijkste Bijdragen

1. Definitie van $EL^\rightarrow$: De auteurs introduceren een nieuwe, tractabele logica genaamd $EL^\rightarrow$. Deze logica is een extensie van $EL$ met verzwakte versies van negatie, disjunctie en universele restrictie.
2. Categorische Semantiek voor SH: Ze presenteren een volledige categorische semantiek voor de expressieve logica SH (inclusief transitive rollen en rollen-inclusie) en bewijzen de equivalentie met de traditionele verzamelingstheoretische semantiek.
3. Tractabiliteitsbewijs: Ze bewijzen dat het controleren van consistentie in $EL^\rightarrow$ polynomiaal is in de grootte van de ontologie. Dit wordt bereikt doordat de verzwakte constructoren geen exponentiële explosie van nieuwe objecten (rollen of concepten) genereren tijdens het redeneren.
4. Expressiviteit: $EL^\rightarrow$ is strikt expressiever dan $EL^\circ_\bot$ (EL met bottom-concept en transitive rollen) en kan negatieve kennis modelleren zonder de complexiteit van volledige SH te accepteren.
5. Onafhankelijkheid: Ze tonen aan dat de verzwakte constructoren onafhankelijk zijn van de andere constructoren in de logica, wat betekent dat $EL^\rightarrow$ zowel "van boven naar beneden" (uit SH door eigenschappen weg te laten) als "van onder naar boven" (uit $EL^\circ_\bot$ door eigenschappen toe te voegen) kan worden gedefinieerd.

Resultaten

• Equivalentie: Er is bewezen dat een SH-ontologie verzamelingstheoretisch inconsistent is dan en slechts dan als deze categorisch inconsistent is.
• Complexiteit: Het redeneerproces voor $EL^\rightarrow$ (gebaseerd op een set van categorische regels) heeft een polynomiale complexiteit. In tegenstelling tot de standaard SH, waar het aantal gegenereerde objecten exponentieel kan groeien door de interactie van $\forall$ en $\sqcup$, blijft dit in $EL^\rightarrow$ beperkt tot een polynoom.
• Praktische Toepasbaarheid: De auteurs tonen aan dat de verzwakte eigenschappen voldoende zijn voor biomedische ontologieën. In de meeste medische ontologieën (zoals SNOMED-CT) komt $n$-voudige disjunctiviteit ($n \ge 3$) zelden of nooit voor; binaire disjunctiviteit (conflict tussen twee concepten) is echter veelvoorkomend en wordt door $EL^\rightarrow$ correct gehanteerd.
• Voorbeeld: In een scenario waar een patiënt zowel een behandeling krijgt als allergisch is voor die behandeling, kan $EL^\rightarrow$ de inconsistentie detecteren (via binaire disjunctiviteit) zonder de rekenkracht van een volledige SH-redeneraar nodig te hebben.

Betekenis en Toekomstperspectief

• Nieuwe Paradigma: Dit werk biedt een fundamenteel nieuw perspectief op de complexiteit van Beschrijvingslogica's. Het toont aan dat ontractabiliteit niet inherent is aan de constructoren zelf, maar aan specifieke interacties die kunnen worden "uitgeschakeld" door de semantiek te verzwakken zonder de praktische bruikbaarheid voor specifieke domeinen (zoals biomedische wetenschap) te verliezen.
• Biomedische Toepassing: Het stelt onderzoekers in staat om negatieve kennis (zoals "geen nier") direct in ontologieën op te nemen met een tractabele redeneerprestatie, wat essentieel is voor het verwerken van grote medische datasets.
• Implementatie: De auteurs plannen de implementatie van een redenerer genaamd Ela voor $EL^\rightarrow$, gebaseerd op bestaande technieken van redenerers zoals ELK. Ze verwachten dat Ela sneller is dan traditionele redenerers voor ontologieën met negatieve kennis, en mogelijk meer instanties terugvindt (door de verzwakte semantiek) die door strikte verzamelingstheoretische redenerers als inconsistent worden afgewezen.
• Theoretische Uitbreiding: De methode opent de deur voor het ontwerpen van andere nieuwe logica's met verschillende complexiteitsklassen door andere categorische eigenschappen te manipuleren, zoals het modelleren van inverse rollen of numerieke restricties.

Kortom, dit artikel presenteert een innovatieve brug tussen abstracte wiskunde (categorie-theorie) en praktische kennisrepresentatie, waardoor het mogelijk wordt om negatieve kennis in complexe domeinen te modelleren zonder de rekenkracht te offeren.