A Non-Binary Method for Finding Interpolants: Theory and Practice

Título: Um Método Não-Binário para Encontrar Interpolantes: Teoria e Prática

Autores: Adam Trybus, Karolina Rożko e Tomasz Skura.
Instituições: Universidade Jagiellonian (Polônia) e Universidade de Zielona Góra (Polônia).

1. O Problema

O artigo aborda o problema da interpolação na lógica proposicional clássica. O Teorema da Interpolação de Craig estabelece que, dadas duas fórmulas $A$ e $B$ tal que $A \to B$ é válida e compartilham pelo menos uma variável proposicional, existe uma fórmula $C$ (o interpolante) construída apenas com as variáveis comuns a $A$ e $B$, tal que $A \to C$ e $C \to B$ são válidas.

Embora existam vários métodos teóricos e práticos para encontrar esses interpolantes (como os sistemas HKP baseados em resolução binária), os autores identificam a necessidade de:

1. Uma prova do teorema que seja mais simples e construtiva.
2. Um método que não dependa estritamente da resolução binária, visando potencialmente reduzir o número de passos computacionais.
3. Uma implementação prática que demonstre a viabilidade de uma abordagem alternativa baseada em sistemas de refutação.

2. Metodologia

A abordagem proposta é inovadora por partir de sistemas de refutação em vez de sistemas de prova tradicionais.

• Sistemas de Refutação: Em vez de provar que uma fórmula é válida, o sistema foca em provar que uma fórmula é não-válida (refutável). O sistema utilizado é baseado em axiomas e regras de refutação que preservam a não-valididade.
• A Ideia Central (Refutação Espelhada): O método trata a busca pelo interpolante como um processo de eliminação de pares de literais ($l$ e $l^*$) de uma fórmula na forma normal.
• Resolução Não-Binária: Diferente dos métodos tradicionais (como HKP) que utilizam resolução binária (eliminando um literal por vez entre duas cláusulas), este método utiliza uma forma de resolução não-binária. As regras de refutação permitem eliminar pares de literais de múltiplas cláusulas simultaneamente, dividindo o problema em dois subproblemas ($G_1$ e $G_2$).
• Propriedade Chave ($\dagger$): A validade de uma fórmula $G$ é equivalente à validade de ambas as suas derivações $G_1$ e $G_2$. Isso permite uma construção indutiva do interpolante.
• Algoritmo:
  1. Transforma-se $A \to B$ em uma forma normal $X \to Y$ (onde $X$ é CNF e $Y$ é DNF).
  2. Identifica-se um par de literais complementares ($l, l^*$) em $X \cup Y^*$.
  3. Aplica-se as regras de refutação para gerar dois novos problemas ($G_1$ e $G_2$) com rank (número de literais conflitantes) menor.
  4. Recursivamente, encontra-se interpolantes para $G_1$ e $G_2$.
  5. Combina-se os interpolantes recursivos usando operadores lógicos ($\land$ ou $\lor$) dependendo da presença dos literais nas fórmulas originais, até atingir casos base (rank 0), onde o interpolante é $\top$ (Verum) ou $\bot$ (Falsum).

3. Principais Contribuições

1. Nova Prova Construtiva: Apresentam uma prova do Teorema da Interpolação baseada em sistemas de refutação, que é considerada mais simples e direta do que as provas existentes na literatura.
2. Método Não-Binário: Introduzem um procedimento de busca de interpolantes que não depende da resolução binária. Isso permite, teoricamente, resolver o problema em menos passos, eliminando múltiplos conflitos de literais de uma só vez.
3. Implementação em Python: Desenvolveram um script em Python que implementa o algoritmo descrito. O código é um "proof-of-concept" (prova de conceito) que lida com fórmulas de até 4 variáveis na versão inicial e foi estendido para um número maior de variáveis.
4. Análise de Desempenho: Realizaram testes empíricos comparando o tempo de execução e o tamanho dos interpolantes gerados sob diferentes configurações de complexidade (número de conjunções e disjunções).

4. Resultados

• Corretude: O algoritmo foi validado teoricamente por indução no "rank" da forma normal clausal. A implementação segue estritamente a lógica teórica, sem otimizações humanas (como atalhos de simplificação), garantindo que o método funcione "puro".
• Desempenho Experimental:
  • Foram gerados e testados milhares de fórmulas aleatórias.
  • Os resultados mostraram uma relação linear entre o tempo de execução e o tamanho das fórmulas de entrada ($X \to Y$) e o tamanho do interpolante resultante.
  • Em testes com 100.000 fórmulas (até 4 variáveis), o tempo médio de execução foi de 0,0032 segundos, com tamanho médio de interpolante de 165 conectivos.
  • Em testes com 50.000 fórmulas (mais complexas), o tempo médio foi de 0,011 segundos.
• Comparação com HKP: O artigo cita um exemplo onde o sistema HKP requer 5 passos para encontrar um interpolante, enquanto o método proposto consegue o mesmo resultado em apenas 2 passos, demonstrando a eficiência potencial da abordagem não-binária.
• Simplificação: Os interpolantes brutos gerados pelo código são frequentemente complexos e contêm redundâncias (ex: $p \lor \bot$), mas o artigo nota que isso é esperado e pode ser simplificado pós-processamento.

5. Significado e Conclusão

O artigo demonstra que os sistemas de refutação, tradicionalmente vistos como ferramentas para provar invalidade, podem ser reutilizados de forma eficaz para construir interpolantes.

• Vantagens: A simplicidade da prova teórica e a natureza construtiva do algoritmo facilitam a implementação prática. A não dependência da resolução binária oferece uma via alternativa que pode ser computacionalmente mais eficiente em certos casos.
• Limitações e Futuro: A implementação atual é básica e os interpolantes gerados não são otimizados esteticamente. O maior desafio futuro identificado pelos autores é estender este método da lógica proposicional para a lógica de primeira ordem (FOL), o que exigiria tanto avanços teóricos quanto adaptações significativas no software.

Em resumo, o trabalho oferece uma nova perspectiva teórica e uma ferramenta prática viável para a interpolação lógica, destacando o potencial de métodos de refutação não-binários na automação de teoremas.