Speakers
Description
Bartosz Bednarczyk, Ian Pratt-Hartmann, and Daumantas Kojelis
Abstract: We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas.
The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment.
We show that the adjacent fragment has the finite model property, and its satisfiability problem is no harder than for the fluted fragment, and hence Tower-complete.
We further show that any relaxation of the adjacency condition on the allowed order of variables in
argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable.
Finally, we study the effect of the adjacency requirement on the well-known guarded fragment GF of first-order logic.
We show that the satisfiability problem for the guarded adjacent fragment (GA) remains TwoExpTime-hard,
thus strengthening the known lower bound for GF, but that, in contrast to GF, the fragment GA
has the Craig Interpolation Property.