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 {...

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Jan Krajícek
• Keywords: Automated Reasoning, CSL 2010, Polynomial Time, Polynomial Time Algorithm, Propositional Proofs