Walnut is a free software program written by Hamoon Mousavi to
solve problems and answer questions, posed in first-order logic,
about automatic and related sequences. It can handle a wide variety
It is available at github.
A manual of how to use it is available on the
There is also a text file with some
how to use Walnut.
If you find Walnut useful in your research, please be sure to cite
Hamoon Mousavi as the author of the software, and let me know what you
achieved with it.
Walnut has been used in a variety of papers. A partial list is here
(will be updated):
- James Currie, Narad Rampersad, Tero Harju, and Pascal Ochem,
Some further results on squarefree arithmetic
progressions in infinite words,
January 18 2019.
- James Currie and Narad Rampersad,
On some problems of Harju concerning squarefree
arithmetic progressions in infinite words,
December 5 2018.
- Lukasz Merta,
Formal inverses of the generalized Thue-Morse sequences
and variations of the Rudin-Shapiro sequence,
October 8 2018.
- Colin Krawchuk and Narad Rampersad,
Cyclic Complexity of Some Infinite Words and Generalizations,
Integers 18A (2018), #A12.
- Jeffrey Shallit and Ramin Zarifi,
Circular critical exponents for Thue–Morse factors,
RAIRO Info. Theor., published online 17 January 2019.
- Pierre Bonardo, Anna E. Frid, Jeffrey Shallit,
"The number of valid factorizations of Fibonacci prefixes",
Theor. Comput. Sci., 2019, to appear.
Available online at https://doi.org/10.1016/j.tcs.2018.12.016.
Jason Bell, Kathryn Hare and Jeffrey Shallit,
When is an automatic set an additive basis?
Proc. Amer. Math. Soc. Ser. B 5 (2018), 50-63.
- Jason Bell, Thomas Finn Lidbetter, and Jeffrey Shallit,
Additive Number Theory via Approximation by Regular Languages,
arxiv preprint, April 23 2018. Appeared in M. Hoshi and S. Seki, eds.,
DLT 2018, LNCS Vol. 11088, Springer, 2018, pp. 121-132.
Here are text files describing how you can verify the results
yourself using Grail and Walnut.
- Narad Rampersad, Jeffrey Shallit, Élise Vandomme,
Critical exponents of infinite balanced words, arxiv preprint,
January 16 2018. Accepted for Theoretical Computer Science; in press
- James Currie, Lucas Mol, and Narad Rampersad,
A family of formulas with reversal of high avoidability index,
International Journal of Algebra and Computation 27 (2017)
- Chen Fei Du, Hamoon Mousavi, Eric Rowland, Luke Schaeffer, and Jeffrey Shallit, Decision Algorithms for Fibonacci-Automatic Words, II: Related Sequences and Avoidability, Theoret. Comput.
Sci. 657 (2017), 146-162.
Examples from the paper that
can be run with Walnut (download Walnut below):
You'll also need to put the following files in the "Word Automata"
- RS.txt (automaton for Rudin-Shapiro)
- P.txt (msd automaton for paperfolding)
- PR.txt (lsd automaton for paperfolding)
- PD.txt (automaton for period-doubling)
- Quentin Valembois, Propriétés décidables des suites automatiques, Master's thesis, University of Liège, Belgium, 2017. Available
- Luke Schaeffer and Jeffrey Shallit,
Closed, Palindromic, Rich, Privileged, Trapezoidal, and Balanced Words in Automatic Sequences, Elect. J. Combinatorics 23 (1) (2016), Paper #P1.25.
- Chen Fei Du, Hamoon Mousavi, Luke Schaeffer, and Jeffrey Shallit,
Decision Algorithms for Fibonacci-Automatic
Words, III: Enumeration and Abelian Properties,
Int. J. Found. Comput. Sci. 27 (8) (2016), 943-963.
- Hamoon Mousavi, Luke Schaeffer, and Jeffrey Shallit,
Decision Algorithms for Fibonacci-Automatic Words, I: Basic Results, RAIRO Inform. Théorique 50
- H. Mousavi and J. Shallit,
Mechanical Proofs of Properties of the Tribonacci Word,
F. Manea and D. Nowotka, eds.,
WORDS 2015, LNCS 9304, Springer, 2015, pp. 1-21. Here are the
Walnut predicates you can use to reproduce most of the results in this
- Daniel Goc, Narad Rampersad, Michel Rigo, Pavel Salimov,
On the number of Abelian Bordered Words (with an Example of Automatic Theorem-Proving)
Int. J. Found. Comput. Sci. 25 (2014), 1097-1110.