Capítulo 1. Introdução 11
é equivalente a NP = CoNP = P SP ACE enquanto para o caso clássico
NP = CoNP . Estas provas devem ser consideradas em sistemas de p rovas que
polinomi al mente simulam sistemas de deduções conhecidos, t ai s como Dedu ção
Natural ou Cálculo de Seqüentes.
A decisão se as iguald ades CoN P = P SP ACE, NP = P SP ACE e
NP = CoN P são válidas ou não é uma tarefa difícil e provoca debates instigant es.
Por outro lado, enquanto não são encontradas as resp ostas para estas questões,
há exemplos bem conhecidos de limites inferiores grandes para provas de tipos
específicos tratadas em certos sistemas de prova. Um caso q ue vale mencionar é
o li mite inferior super po linomial para a prova do Princípio das Casas de Pombos
(doravante P HP ) quando tratado em sistema de provas em Resolução. Este limite
inferior é o mesmo para Cálculo de Seqüentes livres de corte. Este exemplo tem
sido muito út il para argumentar em favor da regra do corte para fornecer provas
em Lógi ca Proposicional, uma vez que tais lim ites inferiores grandes não são
conhecidos para qualquer tautologia proposicional em cálculo de seqüentes com
regra do corte.
Assim, dada uma prova Π em DN, sua correspondente prova normal Π
tem limite inferior hiper-polinomial conhecido com relação ao tamanho de Π bem
como alguns exemplos com limit e inferior hi per-polino mial com relação a Π. Um
destes exemplos pode ser encontrado em Troelst ra (vide (TS00, pp. 215)) e usa a
representação ti pada de numerais de Church para construir um prova de tamanho
polinomi al de uma tautolo gia que tem uma correspond ente prova no rmal que não
pode ser limit e de qualquer função elementar. Para lógica de primeira ordem,
Orekov apresenta exemplos de fórmulas com provas de tamanho linear para o qual
qualquer prova normal tem um limite inferior hiper-polinomial.
Toda esta discussão acima aponta para a necessidade de mecanism os para
comprimir provas. Pode se argumentar sobre o us o de já conhecidos algoritmos de
compactação para tal fato. Contudo, o seu uso é baseado no fato de que a p rova já
seja conhecida. A regra do corte é comum ente colocada de lado em qualquer imple-
mentação de provadores de teoremas, e claramente este é o problema com provas
demasiadamente grandes. O mesmo pode ser dito sob re provadores de teorem as em
Dedução Natural que são feitos para construir provas normais. Para inclusão da re-
gra do corte na implementação ( ou permitir que a imp lementação construa provas
não normais), o implementador deve considerar uma grande quantidade de alt er-
nativas em cada passo da prova. Isto tornará a implementação pouco eficiente. Por
outro lado, se algumas estratégias po n tuais que permitem que a regra do corte (uma
fórmula máxima em terminologia de DN) sejam previamente conhecidas acarreta
implementação melhor do que a anterior, sendo capaz de produzir provas curtas
para casos em que implementações livres do corte não po d em.