Probabilistic verification of proofs in calculuses
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part X, Tome 241 (1997), pp. 97-116
Voir la notice de l'article provenant de la source Math-Net.Ru
The paper defines a special kind of probabilistically checkable proof system, namely, probabilistically checkable proof calculuses (PCP calculuses). A proof in such a calculus can be verified with enough confidence by examining only one random path in the proof tree, without reading the whole proof. The verification procedure
just checks all applications of inference rules along the path; its running time is supposed to be polynomial in the theorem length. It is shown that the deductive power of PCP calculuses is characterized as follows: (i) the decision problem for theorems is in PSPACE for all PCP calculuses, and (ii) this problem is PSPACE-hard for some of them.
@article{ZNSL_1997_241_a3,
author = {E. Ya. Dantsin},
title = {Probabilistic verification of proofs in calculuses},
journal = {Zapiski Nauchnykh Seminarov POMI},
pages = {97--116},
publisher = {mathdoc},
volume = {241},
year = {1997},
language = {ru},
url = {http://geodesic.mathdoc.fr/item/ZNSL_1997_241_a3/}
}
E. Ya. Dantsin. Probabilistic verification of proofs in calculuses. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part X, Tome 241 (1997), pp. 97-116. http://geodesic.mathdoc.fr/item/ZNSL_1997_241_a3/