Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Pinyin
i2Cantonese
i2Cangjie
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

CSL

2010

Springer

2010

Springer

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

Related Content

Added |
08 Nov 2010 |

Updated |
08 Nov 2010 |

Type |
Conference |

Year |
2010 |

Where |
CSL |

Authors |
Jan Krajícek |

Comments (0)