Interpolation in Classical Propositional Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914342722600960 |
|---|---|
| author | Koopmann, Patrick Wernhard, Christoph Wolter, Frank |
| author_facet | Koopmann, Patrick Wernhard, Christoph Wolter, Frank |
| contents | We introduce Craig interpolation and related notions such as uniform interpolation, Beth definability, and theory decomposition in classical propositional logic. We present four approaches to computing interpolants: via quantifier elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_11449 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Interpolation in Classical Propositional Logic Koopmann, Patrick Wernhard, Christoph Wolter, Frank Logic in Computer Science 03B05 (Primary) We introduce Craig interpolation and related notions such as uniform interpolation, Beth definability, and theory decomposition in classical propositional logic. We present four approaches to computing interpolants: via quantifier elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity. |
| title | Interpolation in Classical Propositional Logic |
| topic | Logic in Computer Science 03B05 (Primary) |
| url | https://arxiv.org/abs/2508.11449 |