Separating Counting from Non-Counting in Fragments of Two-Variable First-Order Logic (Extended Abstract)


Kuijer, L ORCID: 0000-0001-6696-9023, Tan, T ORCID: 0009-0005-8341-2004, Wolter, F ORCID: 0000-0002-4470-606X and Zakharyaschev, M ORCID: 0000-0002-2210-5183 (2024) Separating Counting from Non-Counting in Fragments of Two-Variable First-Order Logic (Extended Abstract). .

[thumbnail of dl.pdf] Text
dl.pdf - Open Access published version
Available under License Creative Commons Attribution.
Download (1MB) | Preview

Abstract

We consider the problem of deciding whether two disjoint classes of models defined in a fragment of first-order logic (FO) with counting can be separated in the same fragment but without counting. This problem turns out to be hard. We show that separation for the two-variable fragment FO<sup>2</sup> extended with counting quantifiers by means of plain FO<sup>2</sup> is undecidable, and the same is true of the pair AℒCOℐQ/AℒCOℐ of description logics. On the other hand, we establish 2ExpTime-completeness of the separation problem for the pairs AℒCQ<sup>u</sup>/AℒC<sup>u</sup> and AℒCℐQ<sup>u</sup>/AℒCℐ<sup>u</sup>

Item Type: Conference Item (Unspecified)
Divisions: Faculty of Science and Engineering
Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 24 Oct 2024 08:51
Last Modified: 14 Jun 2025 14:54
Related Websites:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3186208
CORE (COnnecting REpositories)