Uma maneira de provar a NP coNP é mostrar que, para todo sistema de prova proposicional computável em tempo polinomial, existe uma família de tautologias para a qual requer comprimentos de super polinômios (em comparação ao comprimento da tautologia sendo comprovada). Resultados como o de Haken e Ajtai corrigem um sistema de prova proposicional e provam que uma determinada família (PHP neste caso) exige provas de comprimento super polinomial.f f≠≠ffff
Minha pergunta: existem resultados que não consertam um sistema de prova e mostram limites possivelmente muito fracos, mas não triviais, no comprimento da prova? Por exemplo: Existem resultados mostrando que, para todo sistema de prova proposicional, existe uma família de tautologias que requer comprimentos de prova superlineares?
— Karteek
A afirmação é falsa para qualquer família de tautologias reconhecíveis no tempo polinomial: o sistema de provas simplesmente verifica se a fórmula é uma delas e aceita se é. O comprimento da prova deles será O (1). Portanto, acho que nenhum exemplo explícito é conhecido.
Por outro lado, se NP não for igual ao coNP, a família que consiste em todas as tautologias possui um comprimento super polinomial em qualquer sistema de prova eficiente.
Parte do que as pessoas tentam fazer em termos de complexidade profissional é descartar classes interessantes de algoritmos. Um limite inferior em um sistema de prova implica um limite inferior para todos os algoritmos (não-determinísticos) cuja correção pode ser comprovada com eficiência no sistema de prova (se podemos formalizar e provar a correção de um algoritmo para SAT em um sistema de prova, podemos considerar sua falha na execução para encontrar uma tarefa satisfatória como prova da tautologia).
O que exatamente você quer dizer com "limites mais baixos para algoritmos"? E por "algoritmos cuja correção pode ser eficientemente comprovada no sistema de provas", você quer dizer alguma teoria relacionada?
@Karteek, quero dizer limites inferiores no comprimento do histórico de execução, o que implica limites inferiores nos tempos de execução. Refiro-me a sistemas de prova proposicional, mas geralmente há uma teoria relacionada legal em que podemos provar a correção e depois executar uma tradução proposicional para obter uma prova no sistema proposicional de prova.