Partially Finite Model Reasoning in Description Logics Extended Version

1. Formulação do Problema

O artigo aborda a lacuna entre o raciocínio em modelos infinitos (padrão em Lógicas de Descrição, onde os modelos podem ser arbitrariamente grandes) e o raciocínio em modelos finitos (padrão em bancos de dados, onde os domínios são finitos). Embora muitas Lógicas de Descrição (LDs) exibam controlabilidade finita (onde a implicação de consultas é a mesma para modelos finitos e infinitos), outras, como $\mathcal{S}$ (uma extensão de $\mathcal{ALC}$ com papéis transitivos), não o fazem. Nessas lógicas, uma consulta pode ser implicada em todos os modelos finitos, mas não em modelos infinitos, ou vice-versa.

Os autores introduzem o Raciocínio em Modelos Parcialmente Finitos. Neste modo híbrido:

• Uma Base de Conhecimento (BC) é fornecida juntamente com um conceito distinguido $F$.
• A tarefa de raciocínio considera apenas modelos onde a interpretação de $F$ é um conjunto finito de indivíduos.
• O restante do modelo (elementos que não estão em $F$) pode ser infinito.
• Objetivo: Decidir se uma Consulta Conjunção (CC) $Q$ é implicada pela BC sob a restrição de que $F$ é finito (denotado $K \models_F Q$).

Este quadro generaliza tanto a implicação padrão (onde nenhum conceito é restrito) quanto a implicação finita (onde todo o domínio é restrito). Também serve como fundamento teórico para a contenção de consultas com predicados fechados, onde certos predicados são assumidos como tendo extensões finitas.

2. Metodologia

Os autores desenvolvem uma técnica de prova sofisticada para decidir a implicação parcialmente finita para a lógica $\mathcal{S}$. A metodologia envolve várias etapas-chave:

A. Quase-Desenrolamento

Para lidar com modelos infinitos, mantendo a parte "finita" ($F$) gerenciável, os autores introduzem o quase-desenrolamento.

• Diferentemente do desenrolamento padrão (que cria uma árvore duplicando cada nó), o quase-desenrolamento cria uma estrutura semelhante a uma árvore onde elementos críticos (aqueles em $F$) não são duplicados.
• Apenas elementos não críticos são duplicados ao longo dos caminhos. Isso garante que a estrutura resultante tenha um conjunto finito de nós críticos, preservando a propriedade "parcialmente finita", enquanto permite que o restante do modelo seja semelhante a uma árvore para uma análise mais fácil.

B. Interpretações Elementares

Os autores definem uma classe de estruturas finitas chamadas interpretações elementares para servir como representações finitas de potenciais contra-modelos. Estas são construídas hierarquicamente:

1. Singletons/Ciclos/Clusters Críticos: Blocos de construção básicos.
2. Árvores de Loop: Árvores formadas pela fixação de árvores de loop a singletons ou ciclos (semelhantes a cactos).
3. Interpretações Elementares: Árvores construídas pela fixação de árvores de loop e clusters críticos.
   A ideia central é que qualquer contra-modelo pode ser transformado em uma interpretação elementar via quase-desenrolamento sem perder a propriedade de ser um contra-modelo.

C. Bloqueio Colorido e Quocientes

Para lidar com múltiplos papéis transitivos e garantir a existência de um contra-modelo finito com as propriedades requeridas, o artigo adapta o Teorema do Bloqueio Colorido.

• Eles definem uma coloração $k$-esparça de elementos críticos.
• Usando uma relação de equivalência baseada em $k$-vizinhanças, eles constroem uma interpretação quociente.
• Eles provam que, se uma consulta não é satisfeita no modelo infinito original, ela também não é satisfeita no quociente (que é parcialmente finito), desde que a coloração seja suficientemente esparsa.

D. O "Expansão" e Decidibilidade

Para tornar o problema decidível, os autores substituem a condição "o quase-desenrolamento não satisfaz $Q$" por uma condição verificável em uma versão expandida da interpretação elementar ($G_n$).

• Eles "expandem" ciclos na interpretação elementar para um comprimento de $2n+1$ (onde $n$ é o número de variáveis na consulta).
• Eles provam que verificar se a estrutura expandida $G_n$ satisfaz a consulta é equivalente a verificar o quase-desenrolamento para consultas de tamanho $n$.
• Isso permite o uso de um procedimento de eliminação de tipos (semelhante a abordagens baseadas em autômatos) para buscar uma testemunha (um contra-modelo) dentro de um espaço de busca duplamente exponencial.

3. Contribuições Principais

1. Formalização do Raciocínio Parcialmente Finito: O artigo inicia o estudo sistemático do raciocínio onde apenas partes específicas de um modelo são restritas a serem finitas.
2. Resultado de Complexidade para $\mathcal{S}$: Os autores provam que a Implicação de Consulta Parcialmente Finita para $\mathcal{S}$ é 2-ExpTime-completa.
   • Isso corresponde à complexidade tanto da implicação infinita padrão quanto da implicação finita para $\mathcal{S}$, mostrando que o modo híbrido não aumenta a complexidade computacional.
3. Técnicas de Prova Novas: A solução envolve "cirurgia de modelo infinito", combinando quase-desenrolamento, interpretações elementares e bloqueio colorido de uma maneira que vai além da simples combinação de argumentos para os casos finito e infinito.
4. Aplicação a Predicados Fechados: O artigo demonstra que a contenção de consultas na presença de predicados fechados pode ser reduzida à implicação parcialmente finita. Isso fornece um novo limite superior de complexidade para o problema de predicados fechados em LDs expressivas.

4. Resultados

• Teorema Principal (Teorema 16): A implicação parcialmente finita de consultas conjuntivas para a lógica $\mathcal{S}$ é 2-ExpTime-completa.
• Caracterização da Testemunha: Se uma BC não implica parcialmente finita uma consulta, existe uma interpretação "elementar por partes" de tamanho limitado (exponencial no tamanho da BC) cujo quase-desenrolamento serve como contra-modelo.
• Redução: A contenção de consultas com predicados fechados é solucionável em Tempo Polinomial Não Determinístico (NP) dada uma oráculo para implicação parcialmente finita.

5. Significado

• Ponte entre Teoria e Prática: O trabalho preenche a lacuna entre a riqueza teórica dos modelos infinitos (necessária para lógicas expressivas) e as restrições práticas de domínios finitos (necessárias para aplicações em bancos de dados).
• Tratamento de Predicados Fechados: Predicados fechados (onde a extensão de um conceito é conhecida e finita) são cruciais para a integração de bancos de dados e resposta a consultas mediada por ontologias. Este artigo fornece uma base rigorosa de teoria da complexidade para o raciocínio com eles em lógicas expressivas como $\mathcal{S}$.
• Insights de Escalabilidade: O resultado de complexidade (2-ExpTime) sugere que, embora o problema seja difícil, não é indecidível, e os limites superiores alinham-se com sistemas existentes (como SUMA) que utilizam estratégias de materialização parcial.
• Direções Futuras: Os autores sugerem estender essas técnicas para outras lógicas que carecem de controlabilidade finita (por exemplo, $\mathcal{ALCIF}$) e outras tarefas de raciocínio, como contenção de consultas e enumeração.

Em resumo, o artigo estabelece com sucesso que o raciocínio com restrições "parcialmente finitas" é computacionalmente viável e fornece a maquinaria necessária de teoria dos modelos para lidar com a divergência entre modelos finitos e infinitos em Lógicas de Descrição expressivas.