Resolution for Constrained Pseudo-Propositional Logic

Resumo Técnico: Resolução para Lógica Pseudo-Proposicional Restrita

Enunciado do Problema
O artigo aborda as limitações da lógica proposicional padrão e de seus algoritmos SAT associados ao lidar com restrições de contagem. Embora os resolvedores SAT baseados no sistema de prova de resolução sejam altamente eficazes para problemas em verificação formal, planejamento e escalonamento, o poder expressivo da linguagem proposicional padrão é insuficiente para a contagem nativa. Codificar restrições de contagem em Forma Normal Conjuntiva (CNF) tipicamente resulta em um aumento extensivo no número de cláusulas e variáveis, levando a uma complexidade computacional impraticável.

Para mitigar isso, a Lógica Pseudo-Proposicional Restrita (CPPL) foi desenvolvida anteriormente como uma extensão da lógica proposicional. A CPPL integra números naturais e símbolos de restrição em seu alfabeto, permitindo a formulação sucinta de restrições de contagem. No entanto, o sistema de prova existente para a CPPL depende de uma longa lista de regras de inferência (conforme detalhado na Tabela 1 referenciada na literatura de origem), o que é incômodo para implementação computadorizada. Um sistema de prova com menos regras é desejável para reduzir os casos a serem considerados e aumentar a eficiência da implementação.

Metodologia
O artigo propõe um sistema de prova de resolução generalizado especificamente projetado para a CPPL, denominado resolução CPPL. A metodologia envolve:

1. Formalização da Sintaxe e Semântica da CPPL: O trabalho define a linguagem da CPPL, que inclui variáveis proposicionais, números naturais e símbolos de restrição ($>, \ge, =, <, \le$). As sentenças são formadas como triplas $(\phi, \bowtie, n)$, onde $\phi$ é uma fórmula pseudo-proposicional, $\bowtie$ é uma restrição e $n$ é um número natural. As semânticas são definidas via interpretações que mapeiam fórmulas para pares de inteiros representando valores de verdade e contagens.
2. Padronização: O artigo restringe o sistema de resolução a sentenças de "forma padrão", onde a fórmula está em forma normal (uma soma de pseudo-literais) e a restrição é especificamente $\ge$. Nota-se que qualquer sentença CPPL pode ser equivalentemente transformada nesta forma padrão.
3. Redução de Regras: Diferente do sistema anterior com inúmeras regras de inferência, o sistema de resolução CPPL proposto utiliza apenas duas regras de derivação primárias:
   • Regra I (Monotonicidade/Inicial): Lida com relações de subconjunto entre conjuntos de sentenças.
   • Regra II (Resolução): Uma regra de resolução generalizada. Dadas duas sentenças $(\phi_1 + \beta)(\ge, n_1)$ e $(\phi_2 + \neg\beta)(\ge, n_2)$, a regra deriva $(\phi_1 + \phi_2)(\ge, n_1 + n_2 - |\beta|)$. Esta regra efetivamente elimina o literal $\beta$ e sua negação enquanto ajusta o limiar da restrição com base nos coeficientes.
4. Prova de Propriedades: O artigo fornece uma prova construtiva demonstrando que este sistema de duas regras é tanto correto (sentenças derivadas são semanticamente válidas) quanto completo (todas as sentenças semanticamente válidas são deriváveis). A prova de completude baseia-se no Lema de Zorn para estender conjuntos consistentes a conjuntos maximamente consistentes, que são então mostrados como satisfatíveis.

Principais Contribuições

• Generalização da Resolução: O artigo generaliza com sucesso o sistema de prova de resolução proposicional para o domínio da CPPL.
• Conjunto de Regras Minimalista: Estabelece um sistema de resolução para a CPPL que requer apenas duas regras de inferência, simplificando significativamente o framework lógico em comparação com o sistema de múltiplas regras existente anteriormente.
• Corretude e Completude Construtivas: O trabalho fornece uma prova rigorosa e construtiva de que o sistema de resolução CPPL proposto é tanto correto quanto completo.
• Extensão para Cláusulas Infinitas: Um subproduto teórico significativo deste trabalho é a demonstração de que a resolução proposicional permanece correta e completa mesmo quando aplicada a fórmulas com um conjunto infinito de cláusulas, uma propriedade que não é exigida pela CNF padrão, mas que é naturalmente suportada pelo framework da CPPL.

Resultados
O resultado principal é a validação do sistema de resolução CPPL. O artigo prova que para qualquer conjunto de sentenças $S$ e $S'$, se $S$ implica semanticamente $S'$ ($S \models S'$), então $S'$ é derivável de $S$ usando as regras de resolução propostas ($S \vdash_r S'$). A prova utiliza as propriedades de conjuntos maximamente consistentes para preencher a lacuna entre implicação semântica e derivabilidade sintática.

Significância
O artigo afirma que o sistema proposto oferece uma base mais eficiente para o raciocínio automatizado na lógica pseudo-proposicional restrita. Ao reduzir as regras de inferência a um conjunto minimalista análogo à resolução proposicional, o sistema torna-se mais amigável à implementação computadorizada, potencialmente melhorando o desempenho de resolvedores SAT para problemas envolvendo restrições de contagem. Além disso, o trabalho estabelece que a robustez da resolução proposicional se estende além de conjuntos de cláusulas finitos, mantendo sua corretude e completude no contexto de conjuntos de cláusulas infinitos dentro do framework da CPPL.