Congruence properties of combinatorial sequences via Walnut and the Rowland-Yassawi-Zeilberger automaton

TL;DR

This paper demonstrates how Walnut can be used to analyze the congruence properties of well-known combinatorial sequences like Catalan and Motzkin numbers modulo prime powers, leveraging automata theory.

Contribution

It introduces a method to prove properties of combinatorial sequences modulo prime powers using automata and Walnut, including new results and insights.

Findings

Automata can compute Catalan and Motzkin numbers modulo prime powers.

Walnut facilitates automated proofs of sequence properties.

New congruence relations for combinatorial sequences are established.

Abstract

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.