可分解结构的序不变性
Order Invariance on Decomposable Structures
摘要：
顺序不变公式访问结构论域上的顺序，但模型关系与所使用的顺序无关。顺序不变性经常用于计算机科学中基于逻辑的方法。序不变公式捕捉复杂类的无序问题，并且它们对数据库查询的答案与数据库的低级方面的独立性进行建模。我们研究了顺序不变的一元二阶（MSO）和一阶（FO）逻辑的表达能力的限制类的结构，承认某些形式的树分解（不一定有界宽度）。虽然顺序不变的MSO是更有表现力的MSO，甚至，CMSO（MSO与模计数谓词），我们表明，顺序不变的MSO和CMSO是同样有界树宽度的图形和平面图上的表达。这扩展了早期的结果树由于Courcelle。此外，我们表明，所有的性质定义在顺序不变的FO也定义在MSO对这些类。这些结果是一个定理的应用，该定理展示了如何将顺序不变逻辑的可定义性结果从图的树分解的袋子提升到图本身。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
