Order Invariance on Decomposable Structures

DOI10.1145/2933575.2934517zbMATH Open1394.03056arXiv1606.06557OpenAlexW2475308370MaRDI QIDQ4635897FDOQ4635897

Marlin Frickenschmidt, Michael Elberfeld, Martin Grohe

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: Order-invariant formulas access an ordering on a structure's universe, but the model relation is independent of the used ordering. Order invariance is frequently used for logic-based approaches in computer science. Order-invariant formulas capture unordered problems of complexity classes and they model the independence of the answer to a database query from low-level aspects of databases. We study the expressive power of order-invariant monadic second-order (MSO) and first-order (FO) logic on restricted classes of structures that admit certain forms of tree decompositions (not necessarily of bounded width). While order-invariant MSO is more expressive than MSO and, even, CMSO (MSO with modulo-counting predicates), we show that order-invariant MSO and CMSO are equally expressive on graphs of bounded tree width and on planar graphs. This extends an earlier result for trees due to Courcelle. Moreover, we show that all properties definable in order-invariant FO are also definable in MSO on these classes. These results are applications of a theorem that shows how to lift up definability results for order-invariant logics from the bags of a graph's tree decomposition to the graph itself.

Full work available at URL: https://arxiv.org/abs/1606.06557

zbMATH Keywords

finite model theory first-order logic monadic second-order logic planarity bounded tree-width modulo-counting logic order-invariant logic

Mathematics Subject Classification ID

Trees (05C05) Planar graphs; geometric and topological aspects of graph theory (05C10) Model theory of finite structures (03C13) Classical first-order logic (03B10)

Cited In (1)

Successor-Invariant First-Order Logic on Classes of Bounded Degree

This page was built for publication: Order Invariance on Decomposable Structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635897)