Case Study: Saturations as Explicit Models in Equational Theories

1. O Problema

O artigo aborda um desafio fundamental na área de Prova Automática de Teoremas (ATP): a opacidade dos certificados de refutação.

• Contexto: Provedores de teoremas baseados em saturação (como Vampire e E) funcionam deduzindo consequências de um conjunto de fórmulas até encontrar uma contradição (prova) ou atingir um estado de saturação (nenhuma nova consequência não redundante pode ser derivada).
• A Lacuna: Quando uma conjectura é falsa, o ATP atinge a saturação, indicando que um contra-modelo existe. No entanto, o conjunto saturado resultante é frequentemente grande, complexo e "opaco", servindo apenas como um certificado interno difícil de interpretar para humanos.
• Limitação Atual: Embora existam construtores de modelos finitos, muitos problemas em teorias equacionais não possuem modelos finitos; seus contra-modelos são necessariamente infinitos. Os ATPs atuais não conseguem emitir explicitamente esses modelos infinitos, o que impede matemáticos e pesquisadores de entenderem por que uma implicação falha (ex: por que a associatividade não implica a comutatividade).
• Motivação: O Equational Theories Project (ETP) tentou classificar milhões de implicações entre igualdades universalmente quantificadas. Embora os ATPs tenham resolvido a maioria, a falta de contra-modelos explícitos (especialmente infinitos) para os casos não resolvidos por construtores de modelos finitos foi um obstáculo significativo.

2. Metodologia

Os autores propõem uma metodologia para transformar o conjunto saturado de cláusulas em um sistema de reescrita convergente que define explicitamente um modelo (possivelmente infinito).

• Fragmento de Interesse: O foco é no fragmento equacional unitário, que permite apenas igualdades universalmente quantificadas e disequações de termos base (ground).
• Construção do Modelo:
  1. Domínio: O domínio do modelo é o Universo de Herbrand (todos os termos base construídos a partir dos símbolos de função e constantes do problema).
  2. Relação de Igualdade: A igualdade entre dois termos é definida pela sua forma normal. Dois termos são iguais no modelo se, ao serem reescritos usando o conjunto saturado de equações, resultarem no mesmo termo normal.
  3. Normalização: Define-se uma função de normalização computável $J \cdot K$. Dado um termo, aplica-se as regras de reescrita (derivadas das equações saturadas, onde $l \approx r$ e $l \succ r$) até atingir um ponto fixo.
  4. Garantias Teóricas: O método baseia-se em resultados da teoria de reescrita (especificamente unfailing completion e superposition). Se o ATP atinge a saturação sem derivar falsidade, o conjunto de equações resultante é conflituente e terminante (no conjunto de termos base), garantindo que a forma normal seja única e bem-definida.
• Implementação: Os autores modificaram os provadores Vampire e E para:
  • Detectar quando a saturação é atingida sem refutação.
  • Extrair as equações orientadas ($l \succ r$) do conjunto saturado.
  • Emitir essas equações como um sistema de reescrita explícito.

3. Contribuições Chave

1. Exposição de Modelos Infinitos: A principal contribuição é tornar acessível a construção de modelos infinitos a partir de saturações de ATPs, algo que era conhecido teoricamente, mas pouco explorado na prática e desconhecido para muitos usuários.
2. Ponte entre ATP e Matemática: O trabalho permite que matemáticos não especialistas em lógica recebam contra-modelos explícitos (na forma de sistemas de reescrita) para entender falhas em implicações algébricas.
3. Verificação Independente: O sistema de reescrita emitido pode ser verificado por ferramentas externas certificadas para garantir confluência e terminação, validando a correção do modelo gerado pelo ATP.
4. Aplicação ao ETP: A metodologia foi aplicada ao Equational Theories Project, resolvendo casos onde construtores de modelos finitos falharam.

4. Resultados

Os autores aplicaram sua técnica ao conjunto de dados do ETP, focando em 304 problemas que foram refutados apenas por saturação (e não por construtores de modelos finitos).

• Filtragem: Desses 304 casos, 196 foram identificados como "finitamente insatisfiáveis" (sem modelos finitos), restando 108 casos de interesse onde modelos infinitos são necessários.
• Pré-ordenamento: Em 261 dos 304 casos de saturação, as equações já estavam "pré-ordenadas" (o lado esquerdo era maior que o direito segundo a ordem de termos do ATP), permitindo a emissão imediata do sistema de reescrita.
• Certificação:
  • Utilizaram a ferramenta CSI para verificar a confluência (ground confluence).
  • Utilizaram a ferramenta TTT2 para verificar a terminação.
  • Ambas as ferramentas geraram certificados verificáveis pela ferramenta CeTA (baseada na biblioteca Isabelle/IsaFoR).
• Sucesso: Todos os 261 sistemas de reescrita pré-ordenados foram certificados como confluentes e terminantes. Isso fornece 261 contra-modelos infinitos totalmente verificados e confiáveis.
• Caso de Estudo: O artigo detalha a refutação de uma implicação específica (entre as equações 118 e 274 do ETP) que admite apenas modelos infinitos, mostrando o sistema de reescrita gerado que define o contra-modelo.

5. Significado e Impacto

• Confiança em ATPs: Ao permitir a verificação externa dos modelos gerados, o trabalho aumenta a confiança nos resultados de provadores de teoremas complexos, transformando "caixas pretas" em ferramentas transparentes.
• Avanço na Classificação Algébrica: Facilita a classificação de estruturas algébricas ao fornecer contra-exemplos explícitos para implicações que falham, algo crucial para projetos colaborativos como o ETP.
• Futuro: O trabalho abre caminho para extrair modelos de fragmentos lógicos mais ricos (além do equacional unitário) e para a construção explícita de modelos finitos grandes a partir de sistemas de reescrita convergentes.

Em resumo, o artigo demonstra que as saturações de ATPs não são apenas estados de "fim de busca", mas contêm a informação estrutural necessária para construir e verificar explicitamente modelos matemáticos (finitos ou infinitos), preenchendo uma lacuna crítica entre a prova automática e a compreensão humana dos resultados.