Kurucz, Agi, Wolter, Frank 
ORCID: 0000-0002-4470-606X and Zakharyaschev, Michael
(2025)
Deciding the Existence of Interpolants and Definitions in First-Order Modal Logic.
Logical Methods in Computer Science, Volume (4).
ISSN 1860-5974, 1860-5974
|
Text
24-LMCS-final.pdf - Author Accepted Manuscript Available under License Creative Commons Attribution. Download (813kB) | Preview |
Abstract
<jats:p>None of the first-order modal logics between $\mathsf{K}$ and $\mathsf{S5}$ under the constant domain semantics enjoys Craig interpolation or projective Beth definability, even in the language restricted to a single individual variable. It follows that the existence of a Craig interpolant for a given implication or of an explicit definition for a given predicate cannot be directly reduced to validity as in classical first-order and many other logics. Our concern here is the decidability and computational complexity of the interpolant and definition existence problems. We first consider two decidable fragments of first-order modal logic $\mathsf{S5}$: the one-variable fragment $\mathsf{Q^1S5}$ and its extension $\mathsf{S5}_{\mathcal{ALC}^u}$ that combines $\mathsf{S5}$ and the description logic$\mathcal{ALC}$ with the universal role. We prove that interpolant and definition existence in $\mathsf{Q^1S5}$ and $\mathsf{S5}_{\mathcal{ALC}^u}$ is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. These results transfer to the two-variable fragment $\mathsf{FO^2}$ of classical first-order logic without equality. We also show that interpolant and definition existence in the one-variable fragment $\mathsf{Q^1K}$ of first-order modal logic $\mathsf{K}$ is non-elementary decidable, while uniform interpolant existence is again undecidable.</jats:p>
| Item Type: | Article |
|---|---|
| Uncontrolled Keywords: | 46 Information and Computing Sciences |
| Divisions: | Faculty of Science & Engineering Faculty of Science & Engineering > School of Computer Science & Informatics Faculty of Science & Engineering > School of Computer Science & Informatics > Trustworthy Computing |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 13 Oct 2025 08:09 |
| Last Modified: | 02 Nov 2025 08:13 |
| DOI: | 10.46298/lmcs-21(4:6)2025 |
| Related Websites: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3194802 |
Altmetric
Altmetric