From Feasible Proofs to Feasible Computations

12 years 28 days ago
From Feasible Proofs to Feasible Computations
We shall discuss several situations in which it is possible to extract from a proof, be it a proof in a first-order theory or a propositional proof, some feasible computational information about the theorem being proved. This includes extracting feasible algorithms, deterministic or interactive, for witnessing an existential quantifier, a uniform family of short propositional proofs of instances of a universal quantifier, or a feasible algorithm separating a pair of disjoint NP sets. 1 Universal theories Let L be a language that has a function symbol corresponding to every polynomial time algorithm, say as represented by clocked polynomial time Turing machines. We shall assume that polynomial time relations are represented by their characteristic functions and hence the only relation symbol is the equality, which we regard as a logical symbol. Every function symbol from L has a canonical interpretation on the set of natural numbers N which we identify with the set of all binary words {...
Jan Krajícek
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CSL
Authors Jan Krajícek
Comments (0)