  Certain famous combinatorial sequences, such as the Catalan numbers and the
Motzkin numbers, when taken modulo a prime power, can be computed by finite
automata. Many theorems about such sequences can therefore be proved using
Walnut, which is an implementation of a decision procedure for proving various
properties of automatic sequences. In this paper we explore some results (old
and new) that can be proved using this method.
