"202048" . . . "10.1007/s00153-011-0240-0" . "RIV/67985840:_____/11:00369682" . . . "1432-0665" . "Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem"@en . . "P(1M0545), P(IAA100190902), P(LC505), Z(AV0Z10190503)" . "16"^^ . "Archive for Mathematical Logic" . . . "1"^^ . "bounded arithmetic; proof complexity; search problems"@en . "1"^^ . . . "RIV/67985840:_____/11:00369682!RIV12-AV0-67985840" . . . "Thapen, Neil" . . . . . "Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem" . "We give a new characterization of the strict %22Sbjjb sentences provable using Sbkbk induction, for 1 j k. As a small application we show that, in a certain sense, Buss\u2019s witnessing theorem for strict Sbkbk formulas already holds over the relatively weak theory PV. We exhibit a combinatorial principle with the property that a lower bound for it in constant-depth Frege would imply that the narrow CNFs with short depth j Frege refutations form a strict hierarchy with j, and hence that the relativized bounded arithmetic hierarchy can be separated by a family of %22Sb1b1 sentences." . . . . "Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem"@en . . "[396503786D33]" . "We give a new characterization of the strict %22Sbjjb sentences provable using Sbkbk induction, for 1 j k. As a small application we show that, in a certain sense, Buss\u2019s witnessing theorem for strict Sbkbk formulas already holds over the relatively weak theory PV. We exhibit a combinatorial principle with the property that a lower bound for it in constant-depth Frege would imply that the narrow CNFs with short depth j Frege refutations form a strict hierarchy with j, and hence that the relativized bounded arithmetic hierarchy can be separated by a family of %22Sb1b1 sentences."@en . "50" . "7-8" . . "000300094700001" . "Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem" . "DE - Spolkov\u00E1 republika N\u011Bmecko" .