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.
Em sex, 14 de ago de 2020 17:05, Anderson Beraldo de Araújo < andera...@gmail.com> escreveu: > 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 > > > Em qui., 13 de ago. de 2020 às 14:41, Edward Hermann Haeusler < > edward.haeus...@gmail.com> escreveu: > >> 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 >> >> On Thu, Aug 13, 2020 at 10:17 AM Anderson Beraldo de Araújo < >> andera...@gmail.com> wrote: >> >>> 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 >>> >>> >>> Em qui., 13 de ago. de 2020 às 07:29, Edward Hermann Haeusler < >>> edward.haeus...@gmail.com> escreveu: >>> >>>> 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.haeus...@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 <mfin...@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 >>>> >>>> On Wed, Aug 12, 2020 at 10:35 AM Marcelo Finger <mfin...@ime.usp.br> >>>> wrote: >>>> >>>>> >>>>> 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 >>>>> >>>>> Em ter., 11 de ago. de 2020 às 12:40, Edward Hermann Haeusler < >>>>> edward.haeus...@gmail.com> escreveu: >>>>> >>>>>> >>>>>> 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 >>>>>> >>>>>> -- >>>>>> 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+unsubscr...@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 >>>>>> <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANzkscGXA%2BOavSp7zewQBzt1VtfOZci2RKDRCKA2AXpekewRpA%40mail.gmail.com?utm_medium=email&utm_source=footer> >>>>>> . >>>>>> >>>>> >>>>> >>>>> -- >>>>> 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 >>>>> >>>> >>>> >>>> -- >>>> Edward Hermann Haeusler >>>> Associate Professor >>>> Department of Informatics >>>> PUC-Rio >>>> >>>> -- >>>> 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+unsubscr...@dimap.ufrn.br. >>>> 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 >>>> <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANzkscEBMdc_%3DUQ1fBVJgKY02sMz3DRgLgFVarD3DM--iOaP4g%40mail.gmail.com?utm_medium=email&utm_source=footer> >>>> . >>>> >>> >> >> -- >> Edward Hermann Haeusler >> Associate Professor >> Department of Informatics >> PUC-Rio >> > -- > 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+unsubscr...@dimap.ufrn.br. > Para ver essa discussão na Web, acesse > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJrBeCXtRVBkPZDRWkadgWb0bWWDGEOoyRrDPnm8taGsJMkBLA%40mail.gmail.com > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJrBeCXtRVBkPZDRWkadgWb0bWWDGEOoyRrDPnm8taGsJMkBLA%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAEsiyHR03%3DYeE1QrURkqjothMVJyg8X8zjtDZ2WiSbg%3DFP%2B%3D%2BQ%40mail.gmail.com.
