Benedikt, Michael, Kostylev, Egor and Tan, Tony 
ORCID: 0009-0005-8341-2004
(2024)
Two variable logic with ultimately periodic counting.
SIAM Journal on Computing.
![[img]](https://livrepository.liverpool.ac.uk/style/images/fileicons/text.png) |
Text
fo2siam.pdf - Author Accepted Manuscript Access to this file is restricted: awaiting official publication and publisher embargo. Download (908kB) |
Abstract
We consider the extension of FO2 with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence, i.e., the set of the sizes of its finite models, is definable in Presburger arithmetic. In the process we present several refinements to the "biregular graph method". In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.
| Item Type: | Article |
|---|---|
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 15 Apr 2024 07:30 |
| Last Modified: | 15 Apr 2024 07:30 |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3180314 |
Share
Share
