Olá, pessoal. O trabalho de Hermann e Gordeev estava na programação da conferência "General Proof Theory"[1] que aconteceu em Tübingen no ano passado. Contudo, não foi possível aos autores participar da conferência.
Gordeev apresentou o trabalho no seminário do nosso grupo algumas semanas depois. Hudelmaier estava presente. As lâminas[2] da apresentação do Gordeev oferecem um bom panorama geral da demonstração, com foco nos pontos principais. Elas foram publicadas nos anais da conferência[3]. Na ocasião, o manuscrito foi disponibilizado com antecedência, o que nos permitiu acompanhar a apresentação sem muita perplexidade. Na minha opinião, os pontos mais críticos da demonstração, isto é, aqueles que mereceriam uma atenção mais detalhada em busca por erros: a) a afirmação dos autores de que o embutimento do fragmento implicativo do cálculo de sequentes de Hudelmaier no fragmento implicativo de dedução natural preserva as estimativas polinomiais de comprimento e fundamento (nº de fórmulas distintas). Gordeev apresentou o embutimento em detalhes e, para mim, ficou claro que esta parte está correta. Mas aqui é necessário atenção aos detalhes. Quem sabe alguém encontra um escorregão... Curiosamente, a reação inicial de Hudelmaier fora que uso do seu cálculo de sequentes seria inessencial, o que me impressionou um pouco, pois as estimativas polinomiais aqui estão apoiadas no fato de que o comprimento da derivação está restrito a O(n log n). b) após o embutimento das demonstrações CSH (cálculo de sequentes Hudelmaier) para DN (dedução natural), as árvores de DN são horizontalmente compactadas para DAGs (directed acyclic graphs) de maneira que colapsa múltiplas ocorrências de uma mesma fórmula. Esse processo, contudo, resulta em complicações com o descarte de hipóteses. A solução dos autores para este problema está baseada no que eles chamam de "correção local". Esta parte merece atenção. A noção intuitiva de descartes para DAGs é o que os autores chamam de "correção global". Esta noção de descarte, contudo, não pode, em geral, ser verificada em tempo polinomial. Daí, a noção de "correção local" é introduzida como substituta suficiente com verificação polinomial. Confesso que não acompanhei esta parte detalhadamente, embora tenha capturado o funcionamento geral. Este pedaço do argumento, eu diria, é o mais engenhoso do trabalho e merece atenção especial. Eu me prometi passar pelas minúcias depois da apresentação do Gordeev, mas nunca cheguei a fazê-lo. +++ Eu li somente o manuscrito distribuido na conferência em Tübingen, mas dei uma passada de olhos pelo artigo depositado no arXiv. Em comparação com o manuscrito, o artigo parece conter mais material, especialmente exemplos e diagramas ilustrando a compactação (descompactação) para (a partir de) DAGs, bem como uma discussão mais detalhada da questão dos descartes, correção global/local[4]. O Hermann vem trabalhando na intersecção entre complexidade computacional e derivabilidade em CS e DN há um bom tempo. Mas creio que não haja muitas pessoas amplamente familiriazidas com a literatura de ambos os campos. Eu recomendo as referencias nº 7, 1 e 2 do artigo, bem como outros trabalhos do Hermann[5], para quem quiser entender mais sobre o método de compactação para DAGs e a relação entre complexidade, CS e ND. As atualizações recentes na página de divulgação indicam como transferir os resultados obtidos para o âmbito mais conhecido do fragmento existencial de QBF, respondendo aos comentários do Marcelo. Acho ótimo que os colegas estejam interessados na demonstração. É um resultado importante e, quanto mais olhos, melhor. Notas: [1] http://ls.informatik.uni-tuebingen.de/GPT/ [2] Me parece que permaneceu uma pequena falha na última lâmina. Onde se lê "[...] proof of α is verifiable in polynomial time by a non-deterministic algorithm [...]" deveria-se ler ""[...] proof of α is *verifiable* in polynomial time by a *deterministic* algorithm [...]". [3] http://dx.doi.org/10.15496/publikation-10394 [4] A definição 5 (correção global) mencionada na § 3.6.1 parece ter sumido do artigo (embora haja uma discussão no corpo do texto em § 3.4). [5] http://www.tecmf.inf.puc-rio.br/EdwardHermann/Public -- Hermógenes Oliveira -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/87d1j5nb3o.fsf_-_%40camelot.oliveira.
