Kuijer, Louwe 
ORCID: 0000-0001-6696-9023, Tan, Tony ORCID: 0009-0005-8341-2004, Wolter, Frank ORCID: 0000-0002-4470-606X and Zakharyaschev, Michael
(2025)
Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting
In: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2025-6-23 - 2025-6-26, Singapore.
|
Text
25-LICS.pdf - Author Accepted Manuscript Available under License Creative Commons Attribution. Download (246kB) | Preview |
Abstract
For fragments L of first-order logic (FO) with counting quantifiers, we consider the definability problem, which asks whether a given L -formula can be equivalently expressed by a formula in some fragment of L without counting, and the more general separation problem asking whether two mutually exclusive L-formulas can be separated in some counting-free fragment of L. We show that separation is undecidable for the two-variable fragment of FO extended with counting quantifiers and for the graded modal logic with inverse, nominals and universal modality. On the other hand, if inverse or nominals are dropped, separation becomes coNExpTime- or 2ExpTime-complete, depending on whether the universal modality is present. In contrast, definability can often be reduced in polynomial time to validity in L. We also consider uniform separation and show that it often behaves similarly to definability.
| Item Type: | Conference Item (Unspecified) |
|---|---|
| Uncontrolled Keywords: | 5003 Philosophy, 4904 Pure Mathematics, 49 Mathematical Sciences, 50 Philosophy and Religious Studies |
| Divisions: | Faculty of Science & Engineering Faculty of Science & Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 01 Jul 2025 08:12 |
| Last Modified: | 08 Nov 2025 11:46 |
| DOI: | 10.1109/lics65433.2025.00032 |
| Related Websites: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3193486 |
Altmetric
Altmetric