Logical strength of complexity theory and a formalization of the PCP
theorem in bounded arithmeticArticle
Authors: Ján Pich
0000-0002-2731-1330
Ján Pich
We present several known formalizations of theorems from computational
complexity in bounded arithmetic and formalize the PCP theorem in the theory
PV1 (no formalization of this theorem was known). This includes a formalization
of the existence and of some properties of the (n,d,{\lambda})-graphs in PV1.
Rahul Ilango;Jiatu Li;R. Ryan Williams, Proceedings of the 55th Annual ACM Symposium on Theory of Computing, Indistinguishability Obfuscation, Range Avoidance, and Bounded Arithmetic, 2023, Orlando FL USA, 10.1145/3564246.3585187.
Abhishek Jain;Zhengzhong Jin, 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS), Indistinguishability Obfuscation via Mathematical Proofs of Equivalence, 2022, Denver, CO, USA, 10.1109/focs54457.2022.00100.
Cambridge University Press eBooks, The Nature of Proof Complexity, pp. 472-480, 2019, 10.1017/9781108242066.024.
Cambridge University Press eBooks, Basic Example of the Correspondence between Theories and Proof Systems, pp. 165-184, 2019, 10.1017/9781108242066.010.
Cambridge University Press eBooks, Feasible Interpolation: A Framework, pp. 353-383, 2019, 10.1017/9781108242066.019.
Cambridge University Press eBooks, Up to EF via the 〈. . .〉 Translation, pp. 197-210, 2019, 10.1017/9781108242066.012.