Carregant...
Tipus de document
Treball de fi de màsterData de publicació
Llicència de publicació
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
Autors
Director/Tutor
ISSN de la revista
Títol del volum
Recurs relacionat
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
Matèries (anglès)
Citació
Citació
CANTERO DE ARRIBA, Carlos. A Formalization of Kannan’s Circuit Lower Bound in Bounded Arithmetic. [consulta: 2 de gener de 2026]. [Disponible a: https://hdl.handle.net/2445/215181]