Model-checking positive equality free logic on a fixed structure (direttissima)
<|reference_start|>Model-checking positive equality free logic on a fixed structure (direttissima): We give a new, direct proof of the tetrachotomy classification for the model-checking problem of positive equality-free logic parameterised by the model. The four complexity classes are Logspace, NP-complete, co-NP-complete and Pspace-complete. The previous proof of this result relied on notions from universal algebra and core-like structures called U-X-cores. This new proof uses only relations, and works for infinite structures also in the distinction between Logspace and NP-hard under Turing reductions.   For finite domains, the membership in NP and co-NP follows from a simple argument, which breaks down already over an infinite set with a binary relation. We develop some interesting new algorithms to solve NP and co-NP membership for a variety of infinite structures. We begin with those first-order definable in (Q;=), the so-called equality languages, then move to those first-order definable in (Q;<), the so-called temporal languages. However, it is first-order expansions of the Random Graph (V,E) that provide the most interesting examples. In all of these cases, the derived classification is a tetrachotomy between Logspace, NP-complete, co-NP-complete and Pspace-complete.<|reference_end|>
@article{bodirsky2024model-checking,
    title={Model-checking positive equality free logic on a fixed structure
  (direttissima)},
    author={Manuel Bodirsky and Marcin Kozik and Florent Madelaine and Barnaby
  Martin and Michal Wrona},
    journal={arXiv preprint arXiv:2408.13840},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.13840},
    primaryClass={cs.LO}
}