Linear logic proof games and optimization
Bulletin of Symbolic Logic 2 (3):322-338 (1996)
Abstract
§ 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.”DOI
10.2307/420993
My notes
Similar books and articles
A constructive proof of McNaughton's theorem in infinite-valued logic.Daniele Mundici - 1994 - Journal of Symbolic Logic 59 (2):596-602.
The Semantics and Proof Theory of Linear Logic.Arnon Avron - 1988 - Theoretical Computer Science 57 (2):161-184.
Curry-Howard terms for linear logic.Frank A. Bäuerle, David Albrecht, John N. Crossley & John S. Jeavons - 1998 - Studia Logica 61 (2):223-235.
Interpolation in fragments of classical linear logic.Dirk Roorda - 1994 - Journal of Symbolic Logic 59 (2):419-444.
Bidirectional Optimization from Reasoning and Learning in Games.Michael Franke & Gerhard Jäger - 2012 - Journal of Logic, Language and Information 21 (1):117-139.
A new correctness criterion for the proof nets of non-commutative multiplicative linear logics.Misao Nagayama & Mitsuhiro Okada - 2001 - Journal of Symbolic Logic 66 (4):1524-1542.
Quantifiers, anaphora, and intensionality.Mary Dalrymple, John Lamping, Fernando Pereira & Vijay Saraswat - 1997 - Journal of Logic, Language and Information 6 (3):219-273.
Analytics
Added to PP
2009-01-28
Downloads
17 (#641,723)
6 months
2 (#300,644)
2009-01-28
Downloads
17 (#641,723)
6 months
2 (#300,644)
Historical graph of downloads
References found in this work
Computers and Intractability. A Guide to the Theory of NP-Completeness.Michael R. Garey & David S. Johnson - 1983 - Journal of Symbolic Logic 48 (2):498-500.
A game semantics for linear logic.Andreas Blass - 1992 - Annals of Pure and Applied Logic 56 (1-3):183-220.
Decision problems for propositional linear logic.Patrick Lincoln, John Mitchell, Andre Scedrov & Natarajan Shankar - 1992 - Annals of Pure and Applied Logic 56 (1-3):239-311.