Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations
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_ | 1866917629526016000 |
|---|---|
| author | Wolter, Frank Zakharyaschev, Michael |
| author_facet | Wolter, Frank Zakharyaschev, Michael |
| contents | The interpolant existence problem (IEP) for a logic L is to decide, given formulas P and Q, whether there exists a formula I, built from the shared symbols of P and Q, such that P entails I and I entails Q in L. If L enjoys the Craig interpolation property (CIP), then the IEP reduces to validity in L. Recently, the IEP has been studied for logics without the CIP. The results obtained so far indicate that even though the IEP can be computationally harder than validity, it is decidable when L is decidable. Here, we give the first examples of decidable fragments of first-order logic for which the IEP is undecidable. Namely, we show that the IEP is undecidable for the two-variable fragment with two equivalence relations and for the two-variable guarded fragment with individual constants and two equivalence relations. We also determine the corresponding decidable Boolean description logics for which the IEP is undecidable. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_02683 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations Wolter, Frank Zakharyaschev, Michael Logic in Computer Science Logic 03B45 (Primary) 03C40 (Secondary) The interpolant existence problem (IEP) for a logic L is to decide, given formulas P and Q, whether there exists a formula I, built from the shared symbols of P and Q, such that P entails I and I entails Q in L. If L enjoys the Craig interpolation property (CIP), then the IEP reduces to validity in L. Recently, the IEP has been studied for logics without the CIP. The results obtained so far indicate that even though the IEP can be computationally harder than validity, it is decidable when L is decidable. Here, we give the first examples of decidable fragments of first-order logic for which the IEP is undecidable. Namely, we show that the IEP is undecidable for the two-variable fragment with two equivalence relations and for the two-variable guarded fragment with individual constants and two equivalence relations. We also determine the corresponding decidable Boolean description logics for which the IEP is undecidable. |
| title | Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations |
| topic | Logic in Computer Science Logic 03B45 (Primary) 03C40 (Secondary) |
| url | https://arxiv.org/abs/2404.02683 |