An algebraic proof of Rabin's Tree Theorem
We continue the development of a theory of recognisability for infinite trees by introducing the equivalent of a Wilke algebra. As an application we give a new proof of the decidability of the monadic second-order theory of the infinite binary tree, a proof that does not use automata or games. (C) 2013 Elsevier B.V. All rights reserved.
recognisability infinite trees monadic second-order logic