Craig Interpolation for Decidable First-Order Fragments
| Authors |
|
|---|---|
| Publication date | 2024 |
| Host editors |
|
| Book title | Foundations of Software Science and Computation Structures |
| Book subtitle | 27th International Conference, FoSSaCS 2024 : held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024 : proceedings |
| ISBN |
|
| ISBN (electronic) |
|
| Series | Lecture Notes in Computer Science |
| Event | 27th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2024 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 |
| Volume | Issue number | II |
| Pages (from-to) | 137-159 |
| Number of pages | 23 |
| Publisher | Cham: Springer |
| Organisations |
|
| Abstract |
We show that the guarded-negation fragment (GNFO) is, in a precise sense, the smallest extension of the guarded fragment (GFO) with Craig interpolation. In contrast, we show that the smallest extension of the two-variable fragment (FO2), and of the forward fragment (FF) with Craig interpolation, is full first-order logic. Similarly, we also show that all extensions of FO2and of the fluted fragment (FL) with Craig interpolation are undecidable. |
| Document type | Conference contribution |
| Language | English |
| Published at | https://doi.org/10.1007/978-3-031-57231-9_7 |
| Other links | https://www.scopus.com/pages/publications/85190704297 |
| Downloads |
978-3-031-57231-9_7
(Final published version)
|
| Permalink to this page | |
