Craig Interpolation for Decidable First-Order Fragments
| Authors |
|
|---|---|
| Publication date | 2025 |
| Journal | Logical Methods in Computer Science |
| Article number | 22 |
| Volume | Issue number | 21 | 3 |
| Number of pages | 23 |
| Organisations |
|
| Abstract |
We show that the guarded-negation fragment is, in a precise sense, the smallest extension of the guarded fragment with Craig interpolation. In contrast, we show that full first-order logic is the smallest extension of both the two-variable fragment and the forward fragment with Craig interpolation. Similarly, we also show that all extensions of the two-variable fragment and of the fluted fragment with Craig interpolation are undecidable. |
| Document type | Article |
| Language | English |
| Related publication | Craig Interpolation for Decidable First-Order Fragments |
| Published at | https://doi.org/10.46298/lmcs-21(3:22)2025 |
| Other links | https://www.scopus.com/pages/publications/105015320988 |
| Downloads |
2310.08689
(Final published version)
|
| Permalink to this page | |
