Fwd: Proof-theoretic proof of NP=PSPACE?

130 views
Skip to first unread message

Joao Marcos

unread,
Oct 10, 2016, 3:07:14 AM10/10/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Mais detalhes em:

Welcome to NP=PSPACE Area !!!
http://www.tecmf.inf.puc-rio.br/NPPSPACE

JM


---------- Forwarded message ----------

Date: Sat, 8 Oct 2016 10:06:50 -0600
From: Richard Zach <rz...@ucalgary.ca>
To: <f...@cs.nyu.edu>


New on arXiv this week; has anyone read it/formed an opinion?

https://arxiv.org/abs/1609.09562

NP vs PSPACE
Lew Gordeev <https://arxiv.org/find/cs/1/au:+Gordeev_L/0/1/0/all/0/1>,
Edward Hermann Haeusler
<https://arxiv.org/find/cs/1/au:+Haeusler_E/0/1/0/all/0/1>
(Submitted on 30 Sep 2016)

We present a proof of the conjecture $\mathcal{NP}$ =
$\mathcal{PSPACE}$ by showing that arbitrary tautologies of
Johansson's minimal propositional logic admit "small" polynomial-size
dag-like natural deductions in Prawitz's system for minimal
propositional logic. These "small" deductions arise from standard
"large"\ tree-like inputs by horizontal dag-like compression that is
obtained by merging distinct nodes labeled with identical formulas
occurring in horizontal sections of deductions involved. The
underlying "geometric" idea: if the height, $h\left( \partial \right)
$ , and the total number of distinct formulas, $\phi \left( \partial
\right) $ , of a given tree-like deduction $\partial$ of a minimal
tautology $\rho$ are both polynomial in the length of $\rho$, $\left|
\rho \right|$, then the size of the horizontal dag-like compression is
at most $h\left( \partial \right) \times \phi \left( \partial \right)
$, and hence polynomial in $\left| \rho \right|$. The attached proof
is due to the first author, but it was the second author who proposed
an initial idea to attack a weaker conjecture $\mathcal{NP}=
\mathcal{\mathit{co}NP}$ by reductions in diverse natural deduction
formalisms for propositional logic. That idea included interactive use
of minimal, intuitionistic and classical formalisms, so its practical
implementation was too involved. The attached proof of $
\mathcal{NP}=\mathcal{PSPACE}$ runs inside the natural deduction
interpretation of Hudelmaier's cutfree sequent calculus for minimal
logic.

Francisco Antonio Doria

unread,
Oct 10, 2016, 11:18:36 AM10/10/16
to logi...@dimap.ufrn.br
Lew é muito bom. Logo, se tiver engano, é muito sutil. 


--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/CAO6j_LjGy1sfoRZ7tgzZ1Ja97orPipPF79to-__vXMQqO%3D%3Dj0A%40mail.gmail.com.



--
fad

ahhata alati, awienta Wilushati

Marcelo Finger

unread,
Oct 10, 2016, 11:50:10 AM10/10/16
to logi...@dimap.ufrn.br
Olá.

O problema é que um resultado tão quente como NP=PSPACE, para ser aceito pela comunidade hoje em dia, precisa vir com a prova de uma série de resultados correlatos.  

Em particular, o colapso da hierarquia polinomial deve vir junto com uma forma de encontrar a equivalência de uma fórmula da lógica booleana quantificada (QBF), representante de PSPACE, a uma fórmula no fragmento existencial de QBF, representante de NP, de tamanho apenas polinomialmente maior, para um polinômio fixo e independente da fórmula e tendo como parâmetro apenas o tamanho da fórmula.

E, inclusive, deve ficar claro por que o procedimento não serve para eliminar a quantificação totalmente, o que faria com que P=PSPACE.

[]s

Marcelo


Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
--
fad

ahhata alati, awienta Wilushati

--
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+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2BuR7BLwWW8WfeYoRJn0J5A%3DcvnaA26jtmQo_%3DQNMk7dyKXOHA%40mail.gmail.com.



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

Francisco Antonio Doria

unread,
Oct 10, 2016, 12:06:30 PM10/10/16
to logi...@dimap.ufrn.br
Bom, aguardo, interessado é claro, os comentários. 


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 postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2BuR7BLwWW8WfeYoRJn0J5A%3DcvnaA26jtmQo_%3DQNMk7dyKXOHA%40mail.gmail.com.



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

--
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+unsubscribe@dimap.ufrn.br.
 Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CABqmzx2VjNdLw8TBnoUZjrzZznm4uetdqmMdeLDB%2BSTKfPQPhA%40mail.gmail.com.

Alexandre Rademaker

unread,
Oct 10, 2016, 11:07:16 PM10/10/16
to logi...@dimap.ufrn.br
Professor Doria,

Hermann também é muito bom! Os que acompanham de perto sabem que foi o Hermann quem de fato liderou o processo. 


Alexandre 
Sent from my iPhone
--

Francisco Antonio Doria

unread,
Oct 11, 2016, 2:56:35 AM10/11/16
to logi...@dimap.ufrn.br
Peço desculpas por não haver-lo citado, injustiça e erro meus. Deve estar certo sim. 

Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.



--
fad

ahhata alati, awienta Wilushati
--
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+unsubscribe@dimap.ufrn.br.

--
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+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/4F7A6063-495B-4AC2-8D0F-D172A8A36D5E%40gmail.com.

Joao Marcos

unread,
Oct 11, 2016, 9:24:54 AM10/11/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Bem, certamente os nossos colegas estão precisando menos da nossa
*confiança* na correção do resultado e mais da *leitura competente* do
material que produziram...

A propósito, Hermann pediu para avisar que a página
http://www.tecmf.inf.puc-rio.br/NPPSPACE
foi atualizada com material explicativo, e para dizer que "há alguns
problemas de formatação (código tex misturado com wiki), mas é
perfeitamente inteligível".

Francisco Antonio Doria

unread,
Oct 11, 2016, 11:10:00 AM10/11/16
to logi...@dimap.ufrn.br
Gostaria de poder contribuir, mas desconheço as técnicas usadas. 

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

Para postar neste grupo, envie um e-mail para logi...@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/CAO6j_LgdR%2BQkG_6EXQQXdmj0rttxforXPH_u6Hzfs%3DGCj46mVw%40mail.gmail.com.

Eduardo Ochs

unread,
Oct 11, 2016, 11:12:48 AM10/11/16
to logi...@dimap.ufrn.br
Vou contar pro Hermann que ninguém aqui quer ler o paper dele
>> um e-mail para logica-l+u...@dimap.ufrn.br.
>> Para postar neste grupo, envie um e-mail para logi...@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/CAO6j_LgdR%2BQkG_6EXQQXdmj0rttxforXPH_u6Hzfs%3DGCj46mVw%40mail.gmail.com.
>
>
>
>
> --
> fad
>
> ahhata alati, awienta Wilushati
>
> --
> 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 postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Acesse esse grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2BuR7BL0z1UpyGcRNXOD8mknR%3DO9xhPx%3Dy5HeiZLyiOA_4ffxg%40mail.gmail.com.

Marcelo Finger

unread,
Oct 11, 2016, 11:57:35 AM10/11/16
to logi...@dimap.ufrn.br
OI Eduardo.

Pelo contrário, tem várias pessoas tentando entender.  O que eu vi por enquanto é a estratégia da prova.  Eles estão criando um meio de compactar provas na lógica minimal (que é PSPACE-completo) para provas de tamanho sempre polinomial.  Assim sendo, o passo (não-determinístico) inicial da prova poderia ser chutar uma prova de tamanho polinomial, que é verificada tb em tempo polinomial.  Logo a compactação faz PSPACE colapsar para NP.

Só não entendi ainda como funciona essa compactação ...

Marcelo




>> Para postar neste grupo, envie um e-mail para logi...@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/CAO6j_LgdR%2BQkG_6EXQQXdmj0rttxforXPH_u6Hzfs%3DGCj46mVw%40mail.gmail.com.
>
>
>
>
> --
> fad
>
> ahhata alati, awienta Wilushati
>
> --
> 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
--
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+unsubscribe@dimap.ufrn.br.

Para postar neste grupo, envie um e-mail para logi...@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/CADs%2B%2B6hSF9nqaNHJ%2Bha4Mw_rvpQ%3DB-AqRUH7iyCkh9Bdsk8E2A%40mail.gmail.com.

Hermógenes Oliveira

unread,
Oct 12, 2016, 5:57:44 AM10/12/16
to logi...@dimap.ufrn.br
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

Joao Marcos

unread,
Oct 12, 2016, 6:16:25 AM10/12/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
2016-10-12 11:57 GMT+02:00 Hermógenes Oliveira
<hermogene...@student.uni-tuebingen.de>:
> 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.

Bem, há pelo menos um trabalho recente que "chega perto":

Proof complexity of intuitionistic implicational formulas
Emil Jeřábek
Annals of Pure and Applied Logic
Available online 20 September 2016
http://www.sciencedirect.com/science/article/pii/S0168007216301154

Obrigado pela mensagem plena de conteúdo, Hermógenes.

[]s, JM

--
http://sequiturquodlibet.googlepages.com/

Marcelo Finger

unread,
Oct 13, 2016, 7:35:43 AM10/13/16
to logi...@dimap.ufrn.br
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


--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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.

Joao Marcos

unread,
Oct 13, 2016, 8:57:10 AM10/13/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
2016-10-13 13:35 GMT+02:00 Marcelo Finger <mfi...@ime.usp.br>:
> 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.

Acrescento o link para a resposta do Hermann:
http://www.cs.nyu.edu/pipermail/fom/2016-October/020114.html

JM
Reply all
Reply to author
Forward
0 new messages