ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2003)

Paper: Polynomial-time Algorithms from Ineffective Proofs (at LICS 2003)

Authors: Paulo Oliva


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önig’s lemma WKL, and by feasible analysis we mean Cook and Urquhart’s system CPV plus quantifier-free choice QF-AC. We shall also discuss the relation between the system CPV+QF-AC and Ferreira’s 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önig’s lemma for trees defined by \prod {_1^0 }-formulas. Illustrating the applicability of CPV + QF-AC extended with this form of weak König’s 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ödel’s functional interpretation and a novel form of binary bar recursion.


    author = 	 {Paulo Oliva},
    title = 	 {Polynomial-time Algorithms from Ineffective Proofs},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)},
    year =	 {2003},
    month =	 {June}, 
    pages =      {128--137},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2022-10-3113:49
Sam Staton