Prova de NP=PSPACE no Bulletin of Section of Logic

[Edward Hermann Haeusler]

 Caros,

         O Bulletin of the section of Logic (Lodz University, Poland) publicará em breve a nossa prova, do prof. Lew Gordeev e minha, de que NP=PSPACE. O artigo está na seção de EARLY VIEW ainda aguardando a publicação em algum volume a partir (exclusive) do atual. O link para leitura e críticas é

https://czasopisma.uni.lodz.pl/bulletin/article/view/8169

Temos tb  o DOI:

https://doi.org/10.18778/0138-0680.2020.16

         Agradecemos aos editores do Bulletin pela coragem e honestidade de publicar um resultado que pode ter um certo impacto, mesmo que, a despeito do nosso esforço, não conseguiu ser exaustivamente avaliado pela comunidade acadêmica. Explico, o Bulletin enviou nosso submissão para a especialistas (não sei quem são) que após um ano retornaram relatórios de avaliação favoráveis, porém relatarem não terem sido capazes de checar todas os detalhes e que não podem portanto garantir totalmente o resultado. O editor escreveu um remark na primeira página do artigo dizendo que o papel de um periódico científico é também o de divulgar resultados sob estas condições e decidiu pela publicação do artigo. Enfim, o artigo foi avaliado e pede por mais avaliações que serão muito bem vindas....

       Estamos traballhando no sentido de fornecer uma prova mais simples.  Mas aí, já é outra prova.  Esta que está no site do Bulletin não será mais tocada.

Abraços,

Hermann

--

Edward Hermann Haeusler
Associate Professor
Department of Informatics
PUC-Rio

[Valeria de Paiva]

parabens Hermann por ter conseguido chegar a essa publicacao!

abs

Valeria

--
Você recebeu essa mensagem porque está inscrito 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+u...@dimap.ufrn.br.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANzkscGXA%2BOavSp7zewQBzt1VtfOZci2RKDRCKA2AXpekewRpA%40mail.gmail.com.

--

Valeria de Paiva
http://vcvpaiva.github.io/
http://www.cs.bham.ac.uk/~vdp/

[Walter Alexandre Carnielli]

Caro Herrmann.

parabéns pela perseverança, já ouvi vc falar várias vezes sobre
isso, e obviamente não conseguiu passar dos primeiros slides...
Mas vocês fizeram muito bem em tentar e escolher o Bulletin!

Uma pergunta: se fossemos buscar um argumento-matemático, em base de
evidência, não seria possível pensar em benchmarks,
que pudessem levar ao convencimento não-matemático sobre o resultado?

Abraços,
Walter


Em ter., 11 de ago. de 2020 às 18:33, Valeria de Paiva
<valeria...@gmail.com> escreveu:

> Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXub98a7FXFPmN-3HZMZ_ZDxTEh6h3tinzg5nPEOkqwT_A%40mail.gmail.com.

[Famadoria]

Boa! Forte abraço!

Sent from my iPhone

> On 11 Aug 2020, at 22:05, Walter Alexandre Carnielli <walt...@unicamp.br> wrote:
>
> Caro Herrmann.

> --
> 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+u...@dimap.ufrn.br.

> Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAOrCsLcMEGE7WCt%2B-ZYPGZ0DqGwdAQqMqWTcz-V4ZJ_Xq40_PQ%40mail.gmail.com.

[Mauricio Ayala-Rincon]

Caro Hermann,

parabéns pela coragem e perseverância com esse trabalho. Você honra a
nossa comunidade!

Um forte abraço,

Mauricio

[Marcelo Finger]

Olá Hermann.

Eu admiro sinceramente a sua persistência.

Acho que já mencionei a você que a forma de obter reconhecimento pelo seu trabalho é traduzir os resultados de lógicas pouco conhecidas para outras fontes que sejam muito mais mainstream.  No caso da conjectura de  NP=PSPACE, isso se traduz em apresentar um algoritmo que transforma uma fórmula satisfatível em QBF em uma fórmula satisfatível na lógica proposicional clássica de tamanho apenas polinomialmente maior que a fórmula original.  Este resultado é  equivalente a NP=PSPACE, então deve ser possível apresentar um tal algoritmo, o que traria aceitação muito mais ampla do seu resultado.

[]s e continue com o bom trabalho

Marcelo

--

Você recebeu essa mensagem porque está inscrito 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+u...@dimap.ufrn.br.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANzkscGXA%2BOavSp7zewQBzt1VtfOZci2RKDRCKA2AXpekewRpA%40mail.gmail.com.

--

 Marcelo Finger
 Departament of Computer Science, IME    
 University of Sao Paulo
 http://www.ime.usp.br/~mfinger

 ORCID: https://orcid.org/0000-0002-1391-1175
 ResearcherID: A-4670-2009

[Mario Roberto Folhadela Benevides]

Parabéns Hermann!!!

Sua coragem e determinação nos inspiram.

Forte abraço,

Mario

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGG7Aw1xiGU3U%3DoLKKMFKoi07e4iJB93Dx38vFbe5zfrM_upUg%40mail.gmail.com.

--

Federal University of Rio de Janeiro
www.cos.ufrj.br/~mario

[Valeria de Paiva]

Era exatamente isso que eu queria ter escrito, Mario! Valeu!

abs

Valeria

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAMYO67xvQfDYFw-euT%3D1W%2BXY3BnK90_zuUsxYuu7%3DGO-0aXuCA%40mail.gmail.com.

[Edward Hermann Haeusler]

Desculpe, respondi só para o Marcelo, mas acho que interessa a quem já me fez essa pergunta também

Abracos  e bom dia

Hermann

---------- Forwarded message ---------
De: Edward Hermann Haeusler <edward....@gmail.com>
Date: qua, 12 de ago de 2020 10:54
Subject: Re: [Logica-l] Prova de NP=PSPACE no Bulletin of Section of Logic
To: Marcelo Finger <mfi...@ime.usp.br>

Obrigado Marcelo,

     De fato passei um tempo tentando explicitar este algoritmo. Como você sabe essas reduções quando compostas passam a ter uma característica combinatória que não é natural, pois o problema intermediário é mediador simplesmente. Como a nossa técnica é proof-theoretical, somos naturalmente obrigados a sair de uma prova, o que faz a redução  ser para CoNP. Neste caso precisariamos chegar em NP. Claro que o nosso resultado garante CoNP=NP, mas não dá para usa-lo. E uma auto-redução polinomial de Taut para Sat não é conhecida.  O que tenho trabalhado mais próximo do mainstream é justamente em certificados polinomiais para grafos não-hamiltonianos. Aí sim, usa-se a redução de Taut para PSPACE via provabilidade intuicionista e junta-se com esse resultado dos certificados polinomiais. Você tem toda a razão, que para convencer o mainstream em CC deve-se ir por esse caminho. Por outro lado, não posso deixar de divulgar algo que tenho certeza que vale, mesmo que o convencimento ainda seja fácil.....

Além do mais, o índice de rejeição do resultado é bem alto, coisas como o colapso da hierarquia polinomial e etc.....

Muito obrigado novamente !!!  

Abraços,

Hermann

[Anderson Beraldo de Araújo]

Caro Hermann,

Muito obrigado por compartilhar seu trabalho, o qual me parece interessante.

Ao critério externo, por assim dizer, de prova de igualdade entre classes de complexidade A e B que o Marcelo mencionou - construir uma redução apropriada entre problemas completos para as classes A e B (o que envolve relacionar dois problemas definidos sobre assinaturas distintas) -, creio ser importante adicionar um critério interno, a saber: construir uma redução do problema completo estudado em A num problema formulado nos termos de A (mesma assinatura) mas que seja equivalente a um problema completo para B. No caso da linguagem da teoria da prova da lógica intuicionista uma possibilidade para cumprir esse critério interno é mostrar como o algoritmo de vocês reduz a provabilidade intuicionista (problema na classe PSPACE) à satisfazibilidade intuicionista (problema na classe NP). Desse modo, pode-se contornar o problema mencionado por você de ter que passar pela classe CoNP.

Tendo em vista esse critério interno, que deve ser satisfeito, estimo que a abordagem de vocês não reduz PSPACE à NP. A razão é a seguinte. A prova original do Statman de que a provabilidade intuicionista é PSPACE-completa faz uma redução desse problema formulado em termos do sistema de dedução natural do Pravitz da lógica minimal intuicionista à semântica de Kripke da lógica modal S4. Em contrapartida vocês usam em pontos cruciais a versão do cálculo de sequentes do Huldemaier que não tem corte. Apesar das pequenas diferenças sintáticas que o sistema do Huldemaier apresenta, elas expressam saltos de classes de complexidade. No caso de vocês, esse salto é da classe PSPACE para NP, que é justamente o que vocês estão tentando provar. Ou seja, sim, parece-me que vocês estão de fato sugerindo reduções interessantes no tamanho da provabilidade intuicionista que as colocam na classe NP, mas isso foi possível porque a própria eliminação do corte embutida no sistema do Huldemaier faz a redução.

Não entrarei em mais detalhes aqui - fico à disposição para conversarmos em particular. De qualquer forma, para quem desejar dar uma espiada no assunto, alguns artigos recentes tais como Beckmann & Buss (2011), Corrected upper bounds for free-cut elimination, que corrige uma longa sequência de artigos com estimativas erradas dos saltos que mencionei acima, e Gore & Thomson (2019), A Correct polynomial translation of S4 into intuitionistic logic, que também corrige uma sequência trabalhos com erros acerca redutibilidade inicialmente abordada pelo Statman em 1979. Como se pode ver, existem muitos mal entendidos nessa seara, sendo, portanto, algo humanamente normal enganar-se. Não estou sugerindo que o trabalho de vocês está totalmente errado - as reduções em si são interessantes -, mas, até onde entendo, ele assume um pequenino detalhe que compromete a intenção de reduzir PSPACE à NP. The details matter!

Abraços, 

Anderson

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANzkscEBMdc_%3DUQ1fBVJgKY02sMz3DRgLgFVarD3DM--iOaP4g%40mail.gmail.com.

[Walter Alexandre Carnielli]

Colegas:
No intuito de continuar discussão sobre este importantíssimo
resultado do Lev e do Hermann, só gostaria de notar que o argumento
do Anderson apontando um possível erro esbarra em outras tentativas
que também acreditam que NP = PSPACE . O artigo (draft) abaixo
define um problema chamado ODDPATH-HORNUNSAT e mostra que este
problema está em NP e é PSPACE-completo. Como NP ⊆ PSPACE, e
PSPACE é fechado por reduções, então NP = PS PACE. O argumento
usa reduções, como é mais usual em questões de complexidade, ao invés
de teoria da prova (ou da demonstração). Não sou capaz de saber se o
argumento é correto, mas indico como uma evidência favorável.

NP versus PSPACE
Frank Vega
https://hal.archives-ouvertes.fr/hal-01196489/file/NP-versus-PSPACE.pdf

Abraços,
Walter

Em qui., 13 de ago. de 2020 às 10:17, Anderson Beraldo de Araújo
<ande...@gmail.com> escreveu:

> Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJrBeCVWuNHAYC-5V%2B-FboiLdBRYNh6zD1%3DAN%3DbZryYzbtKcSA%40mail.gmail.com.

[Edward Hermann Haeusler]

Caro Anderson,

    Obrigado pelas observações é isso mesmo que eu queria. Vamos lá, nossa prova não é baseada em redução , mas sim em mostrar que qualquer tautologia da lógica minimal  puramente implicacional, que tem validade como sendo PSPACE-completa,  possui um certificado de tamanho polinomial que pode ser verificado em tempo polinomial, ou seja uma prova de tamanho polinomial que é verificável em tempo polinomial.  Não usamos redução, usamos a própria definição da classe NP. O problema SAT na lógica minimal, e portanto no fragmento implicacional, é trivial, pois toda fórmula é satisfatível.  Não dá para fazer nenhuma redução interessante com esse SAT. A simulação polinomial de lógica Intuicionista em lógica minimal implicacional é preserva atutologias, ela não funciona preserva satisfatibilidad, como já comentado. O ponto central da nossa prova é o colapso de uma prova normal em DEDUÇAO NATURAL, da logica puramente minimal em uma estrutura de dag (grafo dirigido) de tamanho polinomial no tamanho da tautologia. O resultado do Hudelmaier é usado somente para garantir que a altura da prova é 18n, onde n é o tamanho da tautologia (comprimento do string que representa a fórmula), mesmo que seu tamanho seja  super-polinomial. Se você verificar, desde a nossa primeira publicação no Studia Logica, isso é feito por um mapeamento das provas em cálculo de sequentes, no fragmento implicacional  do Hudelmaier em Dedução Natural minimal implicacional. 

   O restante do artigo é a descrição do procedimento não-determinístico que extrai uma prova de tamanho polinomial  do dag compactado.  Na versão com certificado, este é uma sequência de alternativas de caminho em uma caminhamento do topo do grafo para a raiz, o certificado escolhe que alternativas formam uma prova válida. Esta parte é que é a novidade em relação ao nosso primeiro

artigo publicado no Studia Logica e que tenho trabalhado para fazer de forma determinística sem certificados claro.

De importante em relação ao comentário iniciado neste email é que uma reduçao via SAT para minimal implicacional não funciona, pois o procedimento é O(1) para ela. A combinatória de provabilidade em minimal implicacional é bem distinta de SAT clássico ou SAT

intuicionista.

Abraços

Hermann

[Claus Akira Horodynski Matsushigue]

Prezado amigo Herman!!!

(Não sei por que os e-mails só foram enviados em privado. Repasso aqui.)

Pois é, o problema é exatamente a interface entre o resultado anterior e o de vocês. Os passos que vocês fizeram são interessantes e perspicazes. Mas o "pulo-do-gato" é justamente a utilização do resultado anterior.

Um forte abraço, 

Claus

Livre de vírus. www.avg.com.

On Fri, Aug 14, 2020 at 6:01 AM Edward Hermann Haeusler <edward....@gmail.com> wrote:

Oi Claus,

Muito obrigado.

É fato que o procedimento nao-deterministico resolve. O dag de tamanho polinomial que representa o colapso da prova super-polinomial é o mesmo da publicacao anterior.... O uso de um certificado polinomial para sua leituura verificacao como prova é que é novo neste artigo recem publicado. O artigo anterior nao falava em prova de NP=PSPACE como tendo sido provada. Este entretanto completa esse passo.

Os detalhes estão lá no artigo que aguarda volume, mas que já pode ser lido.

Note que uma prova por reducao é outra prova, nao é a que fizemos. 

abs

Hermann

Em qui, 13 de ago de 2020 21:22, Claus Akira Horodynski Matsushigue <clau...@mat.unb.br> escreveu:

Pois é grande e querido Hermann...

Quando você fez a apresentação na UnB, já há alguns pares de anos, fiz restrição a este fato e disse que não funcionaria. Infelizmente não pude assistir outras apresentações sua, em particular no EBL. Não sei se vocês conseguiram contornar esta questão.

Meu caro...  todo respeito e admiração por ti!

Um imenso abraço, Claus

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANzkscHdhWEvmrML%2B2kUAnOsAFEH23teeBxv2NaLMv99a%2BauRg%40mail.gmail.com.

Livre de vírus. www.avg.com.

[Anderson Beraldo de Araújo]

Caro Walter,

Muito obrigado por indicar o trabalho do Frank Vega. Diferentemente do trabalho do Lev e Hermann, que tem muitos pontos positivos, a proposta do Frank Vega está totalmente errada - caso ele esteja aqui na lista, lamento pelo tom áspero! :)

Primeiro, o Vega errou na estimativa da complexidade do problema ODDPATH-HORNUNSAT. Não está errado dizer que ele está em NP, mas a razão é que esse problema está em P. Ou seja, se ele estivesse certo, teria provado o extraordinário resultado de que P = PSPACE. Para ter uma noção disso - detalhes, como sempre, ficam como exercício para o leitor! -, note que HORNSAT é P-completo e, portanto, HORNUNSAT também. Adicionar a exigência de verificar se o número de nós na interpretação de HORNUNSAT em termos de grafos é par não muda isso pois pode-se registrar a quantidade de nós em qualquer dos algoritmos usuais que resolvem esse problema. Depois basta aplicar divisão módulo 2 com, por exemplo, o algoritmo euclidiano. Não teremos um problema P-completo por conta da exigência das reduções serem logarítmicas para P-completude, mas não sairemos de P. 

Segundo, num gesto de benevolência, se lemos a tentativa do Vega de reduzir GEOGRAPHY à ODDPATH-HORNUNSAT, nota-se que justamente no passo em que deveria ter feito os cálculos da complexidade ele apela a regra de dedução miraculosa: "But, what does this mean?". E não apresenta as contas. Se ele tivesse feito alguns exemplos dos grafos que se propôs a analisar, teria visto que ao aumentar o número de nós, eles rapidamente não cabem mais na folha de papel. O que, pelos razões óbvias, é uma evidência (empírica?) de que PSPACE não é P!

Apesar de eu não gostar do mainstream e ter cedido ao argumento do Marcelo - apelando ao mainstream, Marcelo? Quem diria?! :) -, o meu ponto foi sugerir uma estratégia para o Hermann que talvez possa ajudá-los. Reduções entre problemas completos para diferentes classes são, na verdade, interpretações, ou seja, você precisa associar estruturas com linguagens diferentes; algo complicado. Uma redução é um homomorfismo e, portanto, um caminho mais viável. Por exemplo, se você consegue interpretar k-SAT em alguma estrutura de grafos, 2-SAT e HORNSAT também será interpretável. No entanto, será mais palatável compreender a relação entre k-SAT, 2-SAT e HORNSAT porque eles estão na mesma linguagem, os dos últimos são reduções.

Abraços,

Anderson

[Anderson Beraldo de Araújo]

Caro Hermann,

Muito obrigado por sua resposta. Ainda não tive tempo de ler o artigo de vocês da Studia Logica. Farei isso mais para frente, quando tiver um tempo disponível. Meu comentário baseou-se no artigo que você compartilhou. Depois de ler sua mensagem e espiar o artigo um de vocês, creio que está claro o que está acontecendo. Permita-me indicar alguns pontos gerais nesse sentido, para que todos possam apreciar o assunto.

Primeiro, quando falei da redução da demonstrabilidade intuicionista (IPROV) à satisfazibilidade intuicionista (ISAT), eu estava me referindo à lógica intuicionista proposicional com absurdo, implicação, conjunção e disjunção. Tendo um algoritmo em tempo polinomial não-determinista para demonstrabilidade intuicionista implicacional (iPROV), pode-se aplicar a inversa da interpretação que o Statman define de IPROV para iPROV.

Segundo, no caso de restringir-se à iPROV, de fato não faz sentido fazer a redução à satisfazibilidade intuicionista implicacional (iSAT). Afinal, as regras de dedução natural da implicação clássica e intuicionista são as mesmas! As regras de sequentes mudam um pouco segundo usamos a proposta do Kleene ou, mais eficientemente, do Dyckhoff, mas isso não muda as classes de complexidade. Não obstante, o resultado do Statman não vale para iPROV diretamente, mas sim para uma interpretação de IPROV em iPROV. Mais exatamente, o Statman fez uma interpretação Interpretacao1 de QBF (a versão de SAT para lógica booleana com quantificadores proposicionais, mencionada aqui pelo Marcelo) em IPROV e, depois outra interpretacao2, de IPROV em iPROV. Ou seja, são fórmulas condicionais do tipo Interpretacao2(Interpretacao1(x)) para x em QBF em iPROV que devem ser consideradas para termos um problema PSPACE-completo, não qualquer fórmula em iPROV. Minha sugestão foi analisar o mesmo tipo de fórmula Interpretacao2(Interpretacao1(x)) em iSAT.

Terceiro, o problema não é o uso do sistema do Hudelmaier. O fato de ele não ter a regra do corte é de fato algo correto - se tivesse corte, a proposta estaria, por princípio, equivocada porque essa regra reduz drasticamente o tamanho das provas. O ponto é que ao usar o sistema do Hudelmaier, vocês perdem os detalhes de Interpretacao2(Interpretacao1(x)) nas reduções que vocês fazem para avaliar a complexidade da normalização em dedução natural. Essas reduções são interessantes.

De qualquer forma, enfatizo que seria muita pretensão querer convencê-lo sobre esse assunto com dois ou três emails. Isso é algo que você e o Lev estão desenvolvendo a vários anos. Meu intuito é apenas indicar alguns pontos que podem ajudar a esclarecer a proposta, que, até onde entendo, pode funcionar, mas penso que ainda não funciona.

Abraços,

Anderson

[Tony Marmo]

Eu vejo com muita simpatia trabalhos assim, já que eu mesmo insisto que devemos buscar meios tais que permitam demonstrações as mais breves possíveis. Destarte, esses são assuntos que merecem pelo menos uma atenção cuidadosa.

Não é uma questão de ser fã do Pravitz. 

Tem muitos aspectos positivos nesse artigo, Herman.

Gostei e parabenizo pela obra.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJrBeCXtRVBkPZDRWkadgWb0bWWDGEOoyRrDPnm8taGsJMkBLA%40mail.gmail.com.

[Walter Alexandre Carnielli]

Caro Anderson,

Obrigado pela sua opinião, eu não tenho a menor ideia sobre a corretude do trabalho do Frank Vega. Mas se uma proposta está totalmente errada, qual seria um contra-exemplo? :-)

Abraços

Walter

[Anderson Beraldo de Araújo]

Caro Walter,

Essa pergunta é boa! 

Não sei qual é a resposta geral, mas por "proposta totalmente errada" entendo "proposta cujos eventuais erros não são passíveis de correção". Talvez uma expressão mais comportada seria "proposta metodologicamente errada", ou seja, não se trata de erros pequenos ou graves mas que podem ser corrigidos porque a proposta tem um método promissor. Interpretei seu compartilhamento do trabalho do Vega como um gesto de apoio ao trabalho do Hermann e não como uma tentativa que avaliar o assunto em questão. Somente respondi porque o trabalho do Lev e Hermann tem um método promissor, ao passo que o do Vega não - lamento mais uma vez pela hostilidade! :)

Em termos conceituais, penso que a proposta do Lev & Hermann pode ser expressa assim: Construir provas intuicionistas é realmente mais difícil do que construir modelos intuicionistas? A julgar pela resposta do Hermann, parece que ele não concebeu o problema dessa forma, mas creio que esse formato põe o trabalho deles numa direção promissora. 

De um ponto de vista formal, interpretações entre problemas completos são em geral mais complicadas de trabalhar. Contudo, com uma perspectiva metodológica clara no âmbito interno das reduções, provas simples baseadas em interpretações podem ser obtidas. Um exemplo notável nesse sentido é a prova do teorema da forma normal de Frobenius que é bastante complicada se feita com álgebra linear, mas interpretando matrizes em grafos direcionados tem-se uma prova bastante simples e intuitiva. O truque da prova da forma normal de Frobenius com grafos não é, porém, a interpretação em grafos (esse é o contexto), mas sim a redução interna do problema de encontrar matrizes de permutação. Acredito que, ao colocar o trabalho do Lev & Hermann nos termos conceituais que sugeri em minhas mensagens, pode-se fazer algo análogo.

Abraços,

Anderson