Paper: Polynomial-time Algorithms from Ineffective Proofs (at LICS 2003)
Authors: Paulo OlivaAbstract
We present a constructive procedure for extracting polynomial-time realizers from ineffective proofs of \prod {_2^0 }-theorems in feasible analysis. By ineffective proof we mean a proof which involves the non-computational principle weak Königs lemma WKL, and by feasible analysis we mean Cook and Urquharts system CPV plus quantifier-free choice QF-AC. We shall also discuss the relation between the system CPV+QF-AC and Ferreiras base theory for feasible analysis BTFA, forwhich \prod {_2^0 }-conservation of WKL has been non-constructively proven. This paper treats the case of weak Königs lemma for trees defined by \prod {_1^0 }-formulas. Illustrating the applicability of CPV + QF-AC extended with this form of weak Königs lemma, we indicate how to formalize the proof of the Heine/Borel covering lemma in this system. The main techniques used in the paper are Gödels functional interpretation and a novel form of binary bar recursion.
BibTeX
@InProceedings{Oliva-PolynomialtimeAlgor, author = {Paulo Oliva}, title = {Polynomial-time Algorithms from Ineffective Proofs}, booktitle = {Proceedings of the Eighteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2003}, year = 2003, editor = {Phokion G. Kolaitis}, month = {June}, pages = {128--137}, location = {Ottawa, Canada}, publisher = {IEEE Computer Society Press} }