A Strategy Language for Controlled Proof Search

Resumo Técnico: Uma Linguagem de Estratégia para Busca de Provas Controlada

Problema
Na dedução automática, a completude estática de um cálculo lógico (a existência de uma prova para qualquer teorema) não garante a completude dinâmica de um provador (a capacidade de realmente encontrar essa prova). Em lógicas semidecidíveis, as regras de inferência podem gerar sucessores infinitos. Se uma estratégia de busca de prova emprega uma exploração injusta — como uma abordagem ingênua de profundidade à esquerda (depth-first) que prioriza indefinidamente um ramo — ela pode adiar inferências relevantes para sempre, falhando em descobrir provas válidas mesmo quando elas existem. Este problema é particularmente agudo em frameworks como o Pgeon, que separam as regras de inferência das estratégias de busca de prova, uma vez que o desenho da política de exploração torna-se um determinante crítico de sucesso.

Metodologia
O artigo introduz uma linguagem de estratégia formal para o Pgeon, um meta-provador que compila especificações declarativas de cálculos lógicos em provadores executáveis. A mudança metodológica central é modelar a busca de prova não como uma relação entre estados, mas como a enumeração de estados de prova via fluxos (streams).

1. Semântica Formal: Um estado de prova ($\Sigma$) é tratado como uma árvore de prova parcialmente construída. Uma estratégia é definida como uma função $s: \Sigma \to \text{Str}(\Sigma)$, mapeando um estado para um fluxo (finito ou infinito) de estados sucessores. Isso torna o não-determinismo explícito:

   • Um fluxo vazio representa falha.
   • Um fluxo unitário representa sucesso determinístico.
   • Um fluxo com múltiplos elementos representa ramificação não-determinística.
   • Fluxos infinitos representam regras que podem gerar sucessores ilimitados.

2. Combinadores: A linguagem fornece um conjunto de operadores para compor essas estratégias, distinguindo entre exploração enviesada (profundidade à esquerda) e justa (intercalada):

   • Composição Sequencial ($;$): Aplica uma estratégia aos resultados de outra.
   • Escolha com Viés à Esquerda ($\parallel$): Tenta a primeira estratégia; se ela falhar (fluxo vazio), recorre à segunda.
   • Composição Sequencial Justa ($\&;$): Intercala os resultados de aplicações sequenciais usando diagonalização ($\triangle$), garantindo que, se um resultado for alcançável em passos finitos, ele será eventualmente explorado.
   • Escolha Justa ($\&|$): Intercala de forma justa os resultados de duas estratégias alternativas.
   • Repetição ($*$): Definida como um ponto fixo inferior usando composição sequencial justa ($\mu X. \text{id} \&; (s \&; X)$), garantindo que todas as profundidades de iteração finitas sejam exploradas em vez de proceder estritamente por profundidade à esquerda.

3. Operações Primitivas: A linguagem inclui regras primitivas ($r$) e um operador de aplicação exaustiva ($r!$) que aplica uma regra a todas as correspondências admissíveis em um estado.

Principais Contribuições

• Semântica de Fluxo Composicional: O artigo fornece uma álgebra composicional para os combinadores de estratégia onde o espaço de busca é reificado como um objeto de primeira classe (um fluxo). Isso permite raciocinar sobre justiça (fairness) e enumeração independentemente de detalhes de implementação como disciplina de pilha ou continuações.
• Mecanismos de Justiça: Ao introduzir operadores de intercalação baseados em diagonalização ($\&;$ e $\&|$), o framework aborda o problema do "esgotamento" (starvation), onde ramos infinitos impedem a descoberta de provas finitas.
• Linguagem de Estratégia Formal para o Pgeon: O trabalho formaliza o componente de estratégia do framework Pgeon, abstraindo o fluxo de controle da busca de prova em uma linguagem declarativa.

Resultos e Estudos de Caso
O artigo demonstra a expressividade e eficácia da abordagem através de dois estudos de caso:

1. Lógica de Primeira Ordem (LK): Os autores abordam a interação entre fechamento (unificação) e saturação de regras. Uma estratégia ingênua de aplicação repetida de regras frequentemente falha em encontrar provas porque se compromete com instanciações específicas precocemente. A estratégia proposta, $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$, utiliza composição justa para intercalar tentativas de fechamento com saturação de regras. Isso garante que diferentes escolhas de unificação sejam exploradas em todas as profundidades de busca, evitando que o sistema fique preso em loops de instanciação infinita enquanto perde uma derivação de fechamento.

2. Lógica Modal (S4): Em S4, a regra não-determinística $\theta$ (remoção arbitrária de fórmulas) é necessária para permitir a aplicação da regra modal S4, mas corre o risco de descartar fórmulas necessárias para o fechamento. Um uso não controlado de $\theta$ leva a becos sem saída. Os autores propõem uma estratégia combinada $\theta^* \&; \text{S4}$, que explora todas as formas de remover fórmulas para permitir aplicações de S4 de forma justa. Isso é integrado a uma estratégia maior $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$, garantindo que, se uma aplicação bem-sucedida de S4 exigir um subconjunto específico de fórmulas removidas, essa configuração seja eventualmente alcançada sem esgotamento.

Significância
O artigo afirma que esta abordagem oferece uma base principiológica e modular para especificar e analisar procedimentos de busca de prova. Ao separar as regras de inferência das estratégias de busca e fornecer uma linguagem formal com semântica composicional, o framework permite a exploração sistemática de espaços de busca em lógicas semidecidíveis. Demonstra que a completude dinâmica pode ser alcançada mesmo quando estratégias ingênuas de profundidade à esquerda falham, ao gerenciar explicitamente a justiça através da intercalação de fluxos. O trabalho permite raciocinar sobre procedimentos de busca de prova em um nível abstrato, independente da implementação específica do provador.