El Dipòsit Digital ha actualitzat el programari. Contacteu amb dipositdigital@ub.edu per informar de qualsevol incidència.

 
Carregant...
Miniatura

Tipus de document

Treball de fi de màster

Data de publicació

Llicència de publicació

cc by-nc-nd (c) Cantero, 2024
Si us plau utilitzeu sempre aquest identificador per citar o enllaçar aquest document: https://hdl.handle.net/2445/215181

A Formalization of Kannan’s Circuit Lower Bound in Bounded Arithmetic

Títol de la revista

ISSN de la revista

Títol del volum

Resum

The aim of this work is to formalize the circuit-size lower bound showed by Kannan in 1982 in a weak theory for feasible computations. In particular, we will work with theories of bounded arithmetic, which are subtheories of Peano Arithmetic that weaken its induction axiom scheme by restricting it to formulas in which the quantifiers are bounded. Kannan’s circuit lower bound states that for every fixed polynomial size of circuits, there is a language in the second level of the polynomial hierarchy that cannot be decided by circuits of that size. We note that the essential ingredient in this proof is a key use of the weak pigeonhole principle, which is available in bounded arithmetic. Instrumental in the proof of Kannan’s Theorem is the celebrated Karp-Lipton’s Theorem, stating that if the satisfiability problem for propositional formulas can be decided by polynomial-size circuits then the polynomial hierarchy collapses to its second level, which we also formalize in the same theory

Descripció

Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2024-2024. Tutor: Albert Atserias

Citació

Citació

CANTERO DE ARRIBA, Carlos. A Formalization of Kannan’s Circuit Lower Bound in Bounded Arithmetic. [consulta: 26 de novembre de 2025]. [Disponible a: https://hdl.handle.net/2445/215181]

Exportar metadades

JSON - METS

Compartir registre