Loading...
Loading...

Go to the content (press return)

Feasibly constructive proofs of succinct weak circuit lower bounds

Author
Muller, M.; Pich, J.
Type of activity
Journal article
Journal
Annals of pure and applied logic
Date of publication
2020-02
Volume
171
Number
2
First page
1
Last page
45
DOI
10.1016/j.apal.2019.102735
Project funding
A unified theory of algorithmic relaxations
Repository
http://hdl.handle.net/2117/177667 Open in new window
URL
https://doi.org/10.1016/j.apal.2019.102735 Open in new window
Abstract
We ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length n. In 1995 Razborov showed that many can be proved in PV1, a bounded arithmetic formalizing polynomial time reasoning. He formalized circuit lower bound statements for small n of doubly logarithmic order. It is open whether PV1 proves known lower bounds in succinct formalizations for n of logarithmic order. We give such proofs in APC1, an extension of PV1 formalizing probabilisti...
Keywords
Approximate counting, Bounded arithmetic, Circuit lower bounds, Natural proofs, Proof complexity

Participants