Portal de Periódicos da CAPES

Computationally Sound Proofs

2000; Society for Industrial and Applied Mathematics; Volume: 30; Issue: 4 Linguagem: Inglês

10.1137/s0097539795284959

1095-7111

Silvio Micali,

Computability, Logic, AI Algorithms

This paper puts forward a new notion of a proof based on computational complexity and explores its implications for computation at large. Computationally sound proofs provide, in a novel and meaningful framework, answers to old and new questions in complexity theory. In particular, given a random oracle or a new complexity assumption, they enable us to prove that verifying is easier than deciding for all theorems; provide a quite effective way to prove membership in computationally hard languages (such as ${\cal C}o$-$\cal N \cal P$-complete ones); and show that every computation possesses a short certificate vouching its correctness. Finally, if a special type of computationally sound proof exists, we show that Blum's notion of program checking can be meaningfully broadened so as to prove that $\cal N \cal P$-complete languages are checkable.