On the Satisfiability of Local First-Order Logics with Data

TL;DR

This paper investigates the decidability of local fragments of first-order logic over data-structured systems, identifying conditions under which satisfiability remains decidable or becomes undecidable.

Contribution

It introduces local fragments of first-order logic with data, establishing decidability results for radius-1 and characterizing the complexity landscape for existential fragments.

Findings

Decidability of radius-1 local fragment with one diagonal relation

Undecidability results for larger radii

Complexity landscape for existential fragments

Abstract

We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain. Data values can be compared wrt.\ equality. As the satisfiability problem for this logic is undecidable in general, we introduce a family of local fragments. They restrict quantification to the neighbourhood of a given reference point that is bounded by some radius. Our first main result establishes decidability of the satisfiability problem for the local radius-1 fragment in presence of one "diagonal relation". On the other hand, extending the radius leads to undecidability. In a second part, we provide the precise decidability and complexity landscape of the satisfiability problem for the existential fragments of local logic, which are parameterized by the number of data values carried by each element and the radius of the considered neighbourhoods. Altogether, we draw a landscape of formalisms that are suitable for the specification of systems with data and open up new avenues for future research.