Proof Complexity and Feasible Interpolation
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909602095824896 |
|---|---|
| author | Tabatabai, Amirhossein Akbar |
| author_facet | Tabatabai, Amirhossein Akbar |
| contents | This is a survey on propositional proof complexity aimed at introducing the basics of the field with a particular focus on a method known as feasible interpolation. This method is used to construct "hard theorems" for several proof systems for both classical and non-classical logics. Here, a "hard theorem" refers to a theorem in the logic whose shortest proofs are super-polynomially long in the length of the theorem itself. To make this survey more accessible, we only assume a basic familiarity with propositional, modal, and first-order logic, as well as a basic understanding of the key concepts in computational complexity, such as the definitions of the classes $\mathbf{NP}$ and $\mathbf{PSPACE}$. Any additional concepts will be introduced and explained as needed. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_03002 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Proof Complexity and Feasible Interpolation Tabatabai, Amirhossein Akbar Logic Computational Complexity This is a survey on propositional proof complexity aimed at introducing the basics of the field with a particular focus on a method known as feasible interpolation. This method is used to construct "hard theorems" for several proof systems for both classical and non-classical logics. Here, a "hard theorem" refers to a theorem in the logic whose shortest proofs are super-polynomially long in the length of the theorem itself. To make this survey more accessible, we only assume a basic familiarity with propositional, modal, and first-order logic, as well as a basic understanding of the key concepts in computational complexity, such as the definitions of the classes $\mathbf{NP}$ and $\mathbf{PSPACE}$. Any additional concepts will be introduced and explained as needed. |
| title | Proof Complexity and Feasible Interpolation |
| topic | Logic Computational Complexity |
| url | https://arxiv.org/abs/2505.03002 |