Monadic second order finite satisfiability and unbounded tree-width

2015/05/25 by Kotek, Tomer, Veith, Helmut, Zuleger, Florian
#F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1505.06622

Abstract

The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese (1991). We prove the following problem is decidable: Input: (i) A monadic second order logic sentence α, and (ii) a sentence β in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of α and β may intersect. Output: Is there a finite structure which satisfies α∧β such that the restriction of the structure to the vocabulary of α has bounded tree-width? (The tree-width of the desired structure is not bounded.) As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic extending monadic second order logic with linear cardinality constraints of the form |X₁|+⋯+|X_r|

Related

• Extending Two-Variable Logic on Trees
• Satisfiability of the Two-Variable Fragment of First-Order Logic over Trees
• Weak MSO+U with Path Quantifiers over Infinite Trees
• Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
• The MSO+U theory of (N,