Fitting Horn DL Ontologies to ABox and Query Examples: A Tale of Simulation Quantifiers and Finite Models

1. Definição do Problema

O artigo aborda o Problema de Ajuste de Ontologias no contexto das Lógicas de Descrição (DL).

• Entrada: Uma coleção de exemplos rotulados $E = (E^+, E^-)$, onde:
  • $E^+$ (Exemplos positivos) são pares $(A, q)$ consistindo de um ABox (dados) e uma consulta booleana (Consulta Atômica, Consulta Conjunta ou União de Consultas Conjunções).
  • $E^-$ (Exemplos negativos) são pares semelhantes $(A, q)$.
• Objetivo: Determinar se existe uma ontologia $O$ (em uma linguagem DL específica) tal que:
  • Para todos $(A, q) \in E^+$: $A \cup O \models q$ (A consulta é entida).
  • Para todos $(A, q) \in E^-$: $A \cup O \not\models q$ (A consulta não é entida).
• Linguagens Alvo: Os autores focam em Horn DLs, especificamente $\mathcal{EL}$ e $\mathcal{ELI}$ (permitindo papéis inversos), e suas extensões com o conceito inferior ($\bot$), denotadas como $\mathcal{EL}^\bot$ e $\mathcal{ELI}^\bot$.
• Linguagens de Consulta: Consultas Atômicas (AQs), Consultas Conjunções (CQs) e Uniões de CQs (UCQs).

Isso contrasta com trabalhos anteriores que focavam em DLs expressivas como $\mathcal{ALC}$ e $\mathcal{ALCI}$. Os autores investigam se a migração para Horn DLs computacionalmente mais leves simplifica o problema de ajuste ou introduz novos desafios técnicos.

2. Metodologia e Abordagem Técnica

A metodologia central baseia-se em caracterizações model-teóricas fundamentadas em simulações em vez de homomorfismos.

A. Simulações vs. Homomorfismos

Em DLs expressivas ($\mathcal{ALC}$), as caracterizações de ajuste frequentemente dependem de homomorfismos. No entanto, para Horn DLs ($\mathcal{EL}$, $\mathcal{ELI}$), os autores estabelecem que simulações são a ferramenta correta.

• Desafio: Simulações são "não-locais". Um laço reflexivo em um exemplo pode ser simulado por um caminho infinito em um modelo. Isso cria uma incompatibilidade ao tentar construir ontologias de ajuste finitas, especialmente para $\mathcal{ELI}$.
• Solução: Os autores introduzem Quantificadores de Simulação (especificamente $\exists^{sim}_{\mathcal{L}}$). Estes permitem que a ontologia expresse restrições baseadas na existência de uma relação de simulação, efetivamente fechando a lacuna entre a natureza local dos conceitos $\mathcal{EL}$ e a natureza não-local das simulações.

B. Caracterizações de Existência

O artigo fornece condições necessárias e suficientes para a existência de uma ontologia de ajuste para cada tipo de consulta:

1. Ajuste Baseado em Consistência (ABox apenas):

   • Uma ontologia de ajuste existe se e somente se nenhum ABox de exemplo negativo simular a união de todos os ABoxes de exemplos positivos ($A^- \not\preceq_{\mathcal{L}} A^+$).
   • Isso vale para $\mathcal{EL}^\bot$ e $\mathcal{ELI}^\bot$.

2. Consultas Atômicas (AQs):

   • A condição envolve uma "completude" dos exemplos negativos. Uma ontologia de ajuste existe se e somente se houver uma completude $C$ dos ABoxes negativos tal que:
     • Nenhuma consulta negativa é satisfeita em $C$.
     • Se um exemplo positivo $(A, Q(a))$ simular um estado em $C$, a consulta deve ser satisfeita naquele estado.
   • Isso pode ser decidido aplicando iterativamente uma regra para gerar uma completude canônica única.

3. Consultas Conjunções/União (CQs/UCQs):

   • A caracterização é mais complexa. Requer a existência de uma interpretação finita $I$ (construída como uma união disjunta de modelos de exemplos negativos) tal que:
     • $I$ não satisfaça nenhuma consulta negativa.
     • Para cada exemplo positivo, se existir uma simulação do ABox do exemplo para $I$, a interpretação "desenrolada" derivada dessa simulação deve satisfazer a consulta.
   • Inovação Técnica Chave: Para lidar com a natureza não-local das simulações (onde uma ontologia finita deve capturar comportamentos infinitos), os autores utilizam produtos diretos de interpretações e quantificadores de simulação. Eles constroem ontologias de ajuste usando esses quantificadores para impor que caminhos de simulação específicos levem à satisfação da consulta.

C. Estratégia Algorítmica

• Para $\mathcal{EL}$ e $\mathcal{EL}^\bot$: Os autores reduzem o problema à verificação de entedimento em $\mathcal{EL}^{sim}_\bot$ (Horn DL com quantificadores de simulação). Eles mostram que o entedimento finito nesta lógica está em PTIME. Isso permite um algoritmo $\Sigma^P_2$ (adivinhando a estrutura da ontologia, contra-adivinhando os contra-modelos).
• Para $\mathcal{ELI}$ e $\mathcal{ELI}^\bot$: A presença de papéis inversos quebra a coincidência entre entedimento finito e infinito em quantificadores de simulação. Os autores provam que o entedimento em $\mathcal{ELI}^{sim}_\bot$ é EXPTIME-completo. Consequentemente, o algoritmo de ajuste enumera possibilidades em vez de adivinhar, levando a uma complexidade EXPTIME.

3. Contribuições Principais

1. Classificação de Complexidade:

   • AQs: O ajuste está em PTIME tanto para $\mathcal{EL}$ quanto para $\mathcal{ELI}$.
   • CQs/UCQs: O ajuste é $\Sigma^P_2$-completo para $\mathcal{EL}$ e EXPTIME-completo para $\mathcal{ELI}$.
   • Significado: Essas complexidades são geralmente menores do que para $\mathcal{ALC}$/$\mathcal{ALCI}$ (onde o ajuste de CQ é 2EXPTIME), mas a lacuna entre $\mathcal{EL}$ e $\mathcal{ELI}$ é significativa devido ao tratamento de papéis inversos.

2. Quantificadores de Simulação no Ajuste:
   O artigo demonstra que problemas de ajuste para Horn DLs levam naturalmente à necessidade de quantificadores de simulação. Ele fornece uma análise rigorosa de $\mathcal{ELI}^{sim}_\bot$, provando sua completude EXPTIME, um resultado de interesse independente para a pesquisa em lógica de descrição.

3. Raciocínio sobre Modelos Finitos:
   Os autores esclarecem que, para $\mathcal{ELI}$, a natureza "não-local" das simulações colide com a natureza "local" dos conceitos $\mathcal{ELI}$ finitos. Eles resolvem isso restringindo as caracterizações a interpretações finitas e utilizando raciocínio sobre modelos finitos, o que é crucial para a decidibilidade na presença de papéis inversos.

4. Tamanho das Ontologias de Ajuste:

   • Para AQs e ajuste baseado em consistência, ontologias de ajuste podem ser construídas sem símbolos auxiliares (tamanho polinomial).
   • Para CQs/UCQs, símbolos auxiliares (nomes de papéis novos) são frequentemente necessários para lidar com consultas desconectadas.
   • Com símbolos auxiliares, ontologias de ajuste para $\mathcal{EL}$ podem ter tamanho polinomial.
   • Para $\mathcal{ELI}$ com CQs/UCQs, os limites de tamanho permanecem abertos (potencialmente exponencial ou pior).

4. Resumo dos Resultados (Interpretação da Tabela 1)

Nota: O salto de $\Sigma^P_2$ para EXPTIME para $\mathcal{ELI}$ é impulsionado pela necessidade de lidar com papéis inversos dentro da estrutura de quantificadores de simulação, o que aumenta a complexidade do problema de entedimento subjacente.

5. Significado e Implicações

• Relevância Prática: $\mathcal{EL}$ e $\mathcal{ELI}$ são as fundações de OWL 2 EL e OWL 2 QL, amplamente utilizados em ontologias biomédicas e empresariais. Fornecer algoritmos de ajuste eficientes (PTIME para AQs) apoia a engenharia de ontologias automatizada e a geração de consultas.
• Insight Teórico: O artigo desafia a intuição de que lógicas "mais simples" sempre levam a problemas de ajuste mais simples. Ele mostra que a migração de $\mathcal{ALC}$ para $\mathcal{EL}$ introduz obstáculos técnicos específicos relacionados à localidade dos conceitos vs. a não-localidade das simulações, necessitando de ferramentas avançadas como quantificadores de simulação.
• Engenharia Reversa: Os resultados contribuem para a "Engenharia Reversa de Consultas" e "Aprendizado de Ontologias", oferecendo garantias formais sobre quando um conjunto de exemplos pode ser separado por uma ontologia Horn e quão complexa é essa separação.
• Direções Futuras: Os autores identificam problemas abertos, como os limites exatos de tamanho para o ajuste $\mathcal{ELI}$ com CQs e a extensão desses resultados para outras Horn DLs como $\mathcal{Horn-ALC}$.

Em conclusão, este artigo fornece uma análise abrangente e rigorosa do ajuste de ontologias para Horn DLs, estabelecendo limites de complexidade precisos e introduzindo técnicas model-teóricas inovadoras (quantificadores de simulação e interpretações finitas) para superar as limitações das abordagens padrão baseadas em homomorfismos.