{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:22Z","timestamp":1753894402705,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We study first-order logic over unordered structures whose elements carry a\nfinite number of data values from an infinite domain. Data values can be\ncompared wrt.\\ equality. As the satisfiability problem for this logic is\nundecidable in general, we introduce a family of local fragments. They restrict\nquantification to the neighbourhood of a given reference point that is bounded\nby some radius. Our first main result establishes decidability of the\nsatisfiability problem for the local radius-1 fragment in presence of one\n\"diagonal relation\". On the other hand, extending the radius leads to\nundecidability. In a second part, we provide the precise decidability and\ncomplexity landscape of the satisfiability problem for the existential\nfragments of local logic, which are parameterized by the number of data values\ncarried by each element and the radius of the considered neighbourhoods.\nAltogether, we draw a landscape of formalisms that are suitable for the\nspecification of systems with data and open up new avenues for future research.<\/jats:p>","DOI":"10.46298\/lmcs-20(3:1)2024","type":"journal-article","created":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T15:23:36Z","timestamp":1719933816000},"source":"Crossref","is-referenced-by-count":0,"title":["On the Satisfiability of Local First-Order Logics with Data"],"prefix":"10.46298","volume":"Volume 20, Issue 3","author":[{"given":"Benedikt","family":"Bollig","sequence":"first","affiliation":[]},{"given":"Arnaud","family":"Sangnier","sequence":"additional","affiliation":[]},{"given":"Olivier","family":"Stietel","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,7,2]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13860\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13860\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T15:23:37Z","timestamp":1719933817000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/11538"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,2]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(3:1)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2307.00831v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2307.00831v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2307.00831","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2307.00831","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,7,2]]},"article-number":"11538"}}