Linear logic proof games and optimization

Bulletin of Symbolic Logic 2 (3):322-338 (1996)
  Copy   BIBTEX


§ 1. Introduction. Perhaps the most surprising recent development in complexity theory is the discovery that the class NP can be characterized using a form of randomized proof checker that only examines a constant number of bits of the “proof” that a string is in a language [6, 5, 31, 3, 4]. More specifically, writing ∣x∣ for the length of a string x, a language L in the class NP of languages recognizable in Nondeterministic polynomial time is traditionally given by a polynomial p and a polynomial-time predicate P such that a string x is in L iff there is some string y satisfying P, where ∣y∣ ≤ p. Intuitively, we can think of a string y as a possible proof that x ϵ L, with the predicate P some kind of proof checker that distinguishes good proofs from bad ones. A string x is therefore in a language L ϵ NP if there is a short proof that x ϵ L, and not in L otherwise. The surprising discovery is that the deterministic proof checker that reads the entire input and proof can be replaced by a probabilistic verifier that on input x and possible proof y, where y is presented in a certain way, flips at most O coins and reads at most a constant number of bits of x and y. Obviously, a probabilistic verifier that does not read the whole proof will sometimes make mistakes. However, the surprising and essentially non-intuitive mathematical fact is that for each language L in NP, it is possible to find a polynomial q and verifier V flipping a logarithmic number of coins and reading a constant number of bits such that, for any x ϵ L, there exists y with ∣y∣ ≤ q and with V accepting with probability 1 and, for x ∉ L, there is no y with ∣y∣ ≤ q and with V accepting with probability ≥ 1/4. This idea canalsobeextended to PSPACE [10, 9], using a game that alternates between two players instead of a proof presented by a “single player.”



    Upload a copy of this work     Papers currently archived: 94,623

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Definability of types, and pairs of o-minimal structures.Anand Pillay - 1994 - Journal of Symbolic Logic 59 (4):1400-1409.
Characterization of recursively enumerable sets.Jesse B. Wright - 1972 - Journal of Symbolic Logic 37 (3):507-511.
Induktive Definitionen und Dilatoren.Wilfried Buchholz - 1988 - Archive for Mathematical Logic 27 (1):51-60.
Consequences of the Provability of NP ⊆ P/poly.Stephen Cook & Jan Krajíček - 2007 - Journal of Symbolic Logic 72 (4):1353 - 1371.
K1.1 Is Not Canonical.G. Hughes & M. Cresswell - 1982 - Bulletin of the Section of Logic 11 (3-4):109-112.
Proofs of regular identities.Ewa Graczynska & Francis Pastijn - 1981 - Bulletin of the Section of Logic 10 (1):35-37.
Probability Dynamics.Amos Nathan - 2006 - Synthese 148 (1):229-256.


Added to PP

58 (#273,533)

6 months
24 (#147,636)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

A game semantics for linear logic.Andreas Blass - 1992 - Annals of Pure and Applied Logic 56 (1-3):183-220.

Add more references