Olá. Os eventos recentes sobre a questão NP=PSPACE são os seguintes:
1) Na lista FOM, Alaisdair Urquhart disse que o resultado NP=PSPACE parecia contradizer um resultado de 2007 sobre um exponential lower-bound no tamanho de provas na lógica intuicionista. 2) O Hermann acaba de responder na lista FOM explicando por que não há contradição. O dito resultado trata do número de linhas em provas axiomáticas, a la Hilbert, enquanto que a prova deles trata da compactação de provas em DAGs, e portanto o resultado deles não contradiz o resultado anterior. OU seja, o Hermann parece ter conseguido neutralizar esse ataque. Mas, como eu disse antes, esse resultado só deve ser aceitável pela comunidade se outros resultados correlatos forem demonstrados. Por exemplo, se eles conseguirem mostrar como uma fórmula no fragmento universal (coNP) da lógica booleana quantificada for mostrado equivalente a uma fórmula no fragmento existencial (NP) de tamanho apenas polinomialmente maior. Fiquem ligados! []s Marcelo 2016-10-12 6:57 GMT-03:00 Hermógenes Oliveira < hermogenes.olive...@student.uni-tuebingen.de>: > 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. > -- Marcelo Finger Departament of Computer Science, IME University of Sao Paulo http://www.ime.usp.br/~mfinger -- 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/CABqmzx1rZmPoxd3ar2QheQAkq%3DacptiX2KARupzy%3D_TCysJ8Pw%40mail.gmail.com.
