  Pecan is an automated theorem prover for reasoning about properties of
Sturmian words, an important object in the field of combinatorics on words. It
is capable of efficiently proving non-trivial mathematical theorems about all
Sturmian words.
