On the Completeness of Interpolation Algorithms
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915097840975872 |
|---|---|
| author | Hetzl, Stefan Jalali, Raheleh |
| author_facet | Hetzl, Stefan Jalali, Raheleh |
| contents | Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm $\mathcal{I}$ is \emph{complete} if, for every semantically possible interpolant $C$ of an implication $A \to B$, there is a proof $P$ of $A \to B$ such that $C$ is logically equivalent to $\mathcal{I}(P)$. We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_02829 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | On the Completeness of Interpolation Algorithms Hetzl, Stefan Jalali, Raheleh Logic in Computer Science Logic Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm $\mathcal{I}$ is \emph{complete} if, for every semantically possible interpolant $C$ of an implication $A \to B$, there is a proof $P$ of $A \to B$ such that $C$ is logically equivalent to $\mathcal{I}(P)$. We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic. |
| title | On the Completeness of Interpolation Algorithms |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2402.02829 |