Model Transformations in Decidability Proofs for Monadic Theories

We survey two basic techniques for showing that the monadic second-order theory of a structure is decidable. In the first approach, one deals with finite fragments of the theory (given for example by the restriction to formulas of a certain quantifier rank) and

• Type: Conference
• Year: 2008
• Where: CSL
• Authors: Wolfgang Thomas
• Keywords: Automated Reasoning, Basic Techniques, Certain Quantifier Rank, CSL 2008, Monadic Second-order Theory