Logical aspects of Cayley-graphs: the group case

We prove that a finitely generated group is context-free whenever its Cayley-graph has a decidable monadic second-order theory. Hence, by the seminal work of Muller and Schupp, our result gives a logical characterization of context-free groups and also proves a conjecture of Schupp. To derive this result, we investigate general graphs and show that a graph of bounded degree with a high degree of symmetry is context-free whenever its monadic second-order theory is decidable. Further, it is shown that the word problem of a finitely generated group is decidable if and only if the first-order theory of its Cayley-graph is decidable.