The monadic second-order logic of graphs. I: Recognizable sets of finite graphs (Q2641288)

The paper begins an investigation of the monadic second-order logic of graphs and of sets of graphs, using techniques from universal algebra and the theory of formal languages. The author introduces a recognizable set in a many-sorted algebra, defines graphs and the operations on graphs, and obtains a many-sorted algebra of graphs. Considering graphs as logical structures, the author introduces the counting monadic second- order logic and the associated definable sets of graphs. The main result of the paper says that every definable set of graphs is recognizable. It follows that, for every graph property expressible in counting monadic second-order logic, the set of graphs satisfying this property, and belonging to a given context-free set of graphs forms a context-free set. The author proves that the monadic second-order theory of a context-free set of graphs is decidable. Finally, the author deals with unordered unbounded trees, proves that a set of finite unordered unbounded trees is recognizable iff it is definable in counting monadic second-order logic, and the counting monadic second-order logic is strictly more powerful than the ``ordinary'' one, in arbitrary logical structures.