AN ALGEBRAIC-THEORY OF GRAPH REDUCTION

We show how membership in classes of graphs definable in monadic second-order logic and of bounded treewidth can be decided by finite sets of terminating reduction rules. The method is constructive in the sense that we describe an algorithm that will produce, from a formula in monadic second-order logic and an integer k such that the class defined by the formula is of treewidth less-than-or-equal-to k, a set of rewrite rules that reduces any member of the class to one of finitely many graphs. in a number of steps bounded by the size of the graph. This reduction system yields an algorithm that runs in time linear in the size of the graph. We illustrate our results with reduction systems that recognize some families of outerplanar and planar graphs.