# Complexidade de prova

Em ciência da computação, complexidade de prova é a medida da eficiência dos métodos de prova de teoremas automatizados que é baseado no tamanho das provas que produzem. Os métodos para provar por contradição na lógica proposicional são os mais analisados, Os dois principais problemas considerados na complexidade de prova são se um método de prova pode produzir uma prova polinomial para toda fórmula inconsistente, e se as provas produzidas por um método são sempre de tamanho semelhante a aquelas produzidas por outro método.

## Polinomialidade de provas

Diferentes sistemas de prova proposicional para prova de teoremas em lógica proposicional, tais como o cálculo de sequentes, o método de corte plano, a resolução, o algoritmo DPLL, etc. produzem diferentes provas quando aplicados à mesma fórmula. Complexidade de prova mede a eficácia de um método em termos do tamanho das provas que produz.
Dois pontos fazem o estudo de complexidade de prova não trivial:
* O tamanho de uma prova depende da fórmula que é para ser provada inconsistente;
* Métodos de prova geralmente são famílias de algoritmos, como alguns de seus passos não são univocamente especificados; por exemplo, a resolução é baseada na iteratividade escolhendo um par de clausulas contendo literais opostos e produzindo uma nova clausula que é uma consequência deles; uma vez que vários desses pares pode estar disponível em cada passo, o algoritmo tem de escolher um; essas escolhas afetam o comprimento da prova.
O primeiro ponto é considerado por comparação do tamanho de uma prova de uma fórmula com o tamanho da fórmula. Esta comparação é feita utilizando os pressupostos usuais de complexidade computacional: em primeiro lugar, uma relação de tamanho/tamanho da fórmula de uma prova polinomial significa que a prova é de tamanho similar ao da fórmula; Em segundo lugar, esta proporção é estudada no caso assintótico conforme o tamanho da fórmula aumenta.
O segundo ponto é levado em conta, considerando, para cada fórmula, o mais curto possível, prova que o método considerado pode produzir.
A questão de polinomialidade de provas é se um método sempre pode produzir uma prova de tamanho polinomial no tamanho da fórmula. Caso esse método existe, então NP seria igual a coNP: é por isso que a questão da polinomialidade de provas é considerado importante na complexidade computacional. Para alguns métodos, a existência de fórmulas cujas provas mais curtas são sempre super-polinomiais foi provada. Para outros métodos, é uma questão em aberto.

## Comparação de tamanho de prova

A segunda questão sobre a complexidade de prova é se um método é mais eficiente do que outro. Uma vez que o tamanho da prova depende da fórmula, é possível que um método possa produzir uma prova curta de uma fórmula e apenas provas longas de outra fórmula, enquanto que um segundo método pode ter exatamente o comportamento oposto. Os pressupostos para medição do tamanho das provas em relação ao tamanho da fórmula e considerando apenas as provas mais curtas são também utilizados nesse contexto.
Ao comparar dois métodos de prova, dois resultados são possíveis:
* para cada prova de uma fórmula produzida usando o primeiro método, existe uma prova de tamanho comparável ao da mesma fórmula produzida pelo segundo método;
* existe uma fórmula tal que o primeiro método pode produzir uma prova curta enquanto todas as provas obtidas pelo segundo método são consistentemente maiores;
Diversas provas do segundo tipo envolvem fórmulas contraditórias expressando a negação do princípio da casa dos pombos, ou seja, que os n+1 pombos pode caber em n buracos com nenhum buraco contendo dois ou mais pombos.

## Automatizabilidade

Um método de prova é automatizável se uma das provas mais curtas de uma fórmula pode ser gerada sempre em tempo polinomial (ou sub-exponencial) no tamanho da prova. Alguns métodos, mas não todos, são automatizáveis. Resultados automatizabilidade não estão em contraste com a suposição de que a hierarquia polinomial não entra em colapso, o que iria acontecer se gerar uma prova em tempo polinomial no tamanho da fórmula fosse sempre possível.

## Interpolação

Considere uma tautologia da forma A (x, y) -> B (y, z). A tautologia é verdade para cada escolha de y, e após a fixação de y a avaliação de A e B são independentes, porque são definidos em conjuntos disjuntos de variáveis. Isto significa que é possível definir um circuito de interpolação C (y), de tal modo que tanto A (x, y) -> C (Y) e C (y) -> B (Y, Z) mantem-se. O circuito de interpolação decide se A (x, y) é falsa ou se B (y, z) é verdadeira, por considerar apenas y. A natureza do circuito de interpolação pode ser arbitrária. No entanto, é possível utilizar uma prova da tautologia inicial A (x, y) -> B (y, z) na forma de uma sugestão sobre como construir C. Alguns sistemas de prova (por exemplo, resolução) são referidos como tendo a interpolação eficiente porque a interpolação C (y) é eficientemente computável a partir de qualquer prova da tautologia A (x, y) -> B (y, z) de tal sistema de prova. A eficiência é medida em relação ao comprimento da prova: é mais fácil de calcular interpolantes para provas mais longas, de modo que este parece ser propriedade anti-monótona na resistência do sistema de prova.
A interpolação é uma forma fraca de automação: uma maneira de deduzir a existência de pequenos circuitos a partir da existência de pequenas provas. Em particular, as três seguintes afirmações não podem ser simultaneamente verdadeiras: (a) A (x, y) -> B (y, z) tem uma prova curta em algum sistema de prova; (b) tal sistema de prova tem interpolação eficiente; (c) o circuito de interpolação resolve um problema computacionalmente difícil. É claro que (a) e (b) implica que existe um pequeno circuito de interpolação, que está em contradição com (C). Essa relação permite transformar limites superiores ao comprimento de prova em limites inferiores de computações, e duplamente para transformar algoritmos de interpolação eficientes em limites inferiores no comprimento da prova.

## Lógicas não clássicas

A ideia da comparação dos tamanhos das provas pode ser utilizada para qualquer processo de raciocínio automatizado que gera uma prova. Algumas pesquisas têm sido feitas sobre o tamanho de provas para lógicas proposicionais não clássicas, em particular, intuicionista, modal, e lógicas não monotônicas.

## Veja também

* Automated theorem proving
* Computational complexity
* Intuitionistic logic
* Non-monotonic logic