Walnut is available at github.
After you download it and install it, go to the directory
`Walnut/bin` and type `java Main.prover` to get started.
A manual of how to use it is available on the
arxiv.
There is also a text file with some
examples of
how to use `Walnut`.

Here is a video tutorial
on how to use `Walnut`:

If you are using Walnut under the Eclipse environment, here are a few tips. Download the Walnut software. Start Eclipse up. Use the default workspace. Open "Project" from the File choices, and choose "Walnut". Next, go to src/Main in the menu choices, right-click on prover.java and choose "Run As Java Application". You should now get a window where you can enter Walnut commands. To see results, go to the Eclipse file menu, right-click on "Result" and choose "Refresh" and the results should be there. Thanks to Stepan Holub for this info.

Recently Walnut has been modified by Aseem Baranwal to handle the Pell
number system, and more generally, the Ostrowski number system based
on any quadratic irrational. To use this version of Walnut, visit
https://github.com/aseemrb/walnut. After you download and install it, go to the directory
`Ostrowski/bin` and type `java Main.Prover` to get started.
(Note: for the old Walnut, you use lowercase "p" in prover; for the
new version you use uppercase "P" in prover.)
The command "ost name [0 1 2] [3 4]", for example, defines
an Ostrowski number system for the continued fraction [0,1,2,3,4,3,4,3,4,...].
It can then be used by prefacing a query with "?msd_name" or "?lsd_name".
Aseem Baranwal has prepared a brief summary of his additions to
Walnut here.

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):

- Jarkko Peltomäki and Ville Salo, Automatic winning shifts, Arxiv preprint arXiv:2106.07249 [cs.FL], June 14 2021.
- Jeffrey Shallit,
Frobenius numbers and automatic sequences,
Arxiv preprint arXiv:2103.10904 [math.NT], March 19 2021.
Files for the paper:
- complete Walnut code for all the proofs of the paper
- shift.txt (put this in the "Automata Library" of Walnut)
- fibinc.txt (put this in the "Automata Library" of Walnut)

- Jason P. Bell and J. Shallit, Lie complexity of words, Arxiv preprint, Feb 7 2021, arXiv:2102.03821 [cs.FL]. Available here.
- Aseem Baranwal, Luke Schaeffer, and Jeffrey Shallit,
Ostrowski-automatic sequences: Theory and applications,
*Theor. Comput. Sci.***858**(2021) 122-142. Available here until March 11 2021. - Jeffrey Shallit,
Robbins and Ardila meet Berstel,
*Info. Proc. Letters***167**(2021). Available at https://doi.org/10.1016/j.ipl.2020.106081. - Jeffrey Shallit, Abelian complexity and synchronization, arxiv preprint, November 1 2020. Appeared in
Abelian complexity and synchronization,
*INTEGERS***21**(2021), #A36.

Here are the files associated with the paper:- rst.txt (put this in the Result directory of Walnut)
- TRL.txt (put this in the Word Automata Library)
- Walnut commands for the paper
- TRAC.txt (Walnut DFAO for abelian complexity of Tribonacci word; put in the Word Automata Library directory in order to use it)
- TRAS.txt (Walnut DFAO for subsets of abelian factors of Tribonacci word; put in the Word Automata Library directory in order to use it)

- Jeffrey Shallit,
Subword complexity of the Fibonacci-Thue-Morse sequence: the proof of Dekking's conjecture,
*Indag. Math.***32**(2021), 729-735. Files for the paper:- FTM.txt, put this in the "Word Automata" library of Walnut
- FTMD.txt, put this in the "Word Automata" library of Walnut
- walnut commands
- ftmatrix.mpl, the Maple code for the matrix

- Jeffrey Shallit, Robbins and Ardila meet Berstel, Arxiv preprint 2007.14930, July 29 2020.
- Daniel Gabric and Jeffrey Shallit, The simplest binary word with only three squares, Arxiv preprint 2007.08188, July 17 2020. Data for the paper:
- Marko Milosevic and Narad Rampersad,
Squarefree words with interior disposable factors, Arxiv preprint, July 7 2020. Appeared in
*Theor. Comput. Sci.***863**(2021), 120-126. - Jarkko Peltomäki and Markus A. Whiteland,
Avoiding abelian powers cyclically, Arxiv preprint, June 11 2020. Appeared in
*Advances in Applied Mathematics***121**(2020), 102095. DOI:`10.1016/j.aam.2020.102095. - Aseem Raj Baranwal, Decision algorithms for Ostrowski-automatic sequences, Master's thesis, University of Waterloo, 2020.
- Craig S. Kaplan and Jeffrey Shallit, A Frameless 2-Coloring of the Plane Lattice, Arxiv preprint, May 19 2020. Submitted.
- Jeffrey Shallit, Sumsets of Wythoff sequences, Fibonacci representation, and beyond, arxiv preprint 2006:04177, June 7 2020.
- Aseem Raj Baranwal, Jeffrey Shallit,
Repetitions in infinite palindrome-rich words, arxiv preprint, April 22 2019.
In Mercas R., Reidenbach D. (eds.)
*Combinatorics on Words. WORDS 2019.*Lecture Notes in Computer Science, vol. 11682, Springer, 2019, pp. 93-105. Available here. - Tim Ng, Pascal Ochem, Narad Rampersad, Jeffrey Shallit,
New
results on pseudosquare avoidance, arxiv preprint, April 19 2019.
In Mercas R., Reidenbach D. (eds.)
*Combinatorics on Words. WORDS 2019.*Lecture Notes in Computer Science, vol. 11682, Springer, 2019, pp. 264-274. Available here. - T. Clokie, D. Gabric, and J. Shallit,
Circularly squarefree words and unbordered conjugates: a new approach,
arxiv preprint, April 17 2019.
In Mercas R., Reidenbach D. (eds.)
*Combinatorics on Words. WORDS 2019.*Lecture Notes in Computer Science, vol. 11682, Springer, 2019, pp. 264-274. Available here. - Aseem R. Baranwal, Jeffrey Shallit,
Critical exponent
of infinite balanced words via the Pell number system,
arxiv Preprint, February 1 2019.
In Mercas R., Reidenbach D. (eds.)
*Combinatorics on Words. WORDS 2019.*Lecture Notes in Computer Science, vol. 11682, Springer, 2019, pp. 80-92. Available here. - James Currie, Narad Rampersad, Tero Harju, and Pascal Ochem,
Some further results on squarefree arithmetic
progressions in infinite words,
arxiv preprint,
January 18 2019. Appeared in
*Theoretical Computer Science***799**(2019) 140-148. - James Currie and Narad Rampersad, On some problems of Harju concerning squarefree arithmetic progressions in infinite words, arxiv preprint, December 5 2018.
- Lukasz Merta,
Formal inverses of the generalized Thue-Morse sequences
and variations of the Rudin-Shapiro sequence,
arxiv preprint,
October 8 2018. Appeared in
*Discrete Mathematics and Theoretical Computer Science*Vol. 22:1, 2020, #15. - 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. Available here.
- 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. Available here. - 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 here. - 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) 477-493. - A. Rajasekaran, N. Rampersad, J. Shallit,
Overpals, Underlaps, and Underpals,
in
*WORDS 2017: Combinatorics on Words*, 2017, pp. 17-29. - 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):- Thue-Morse examples
- Rudin-Shapiro examples
- Rudin-Shapiro example for trapezoidal words
- paperfolding sequence examples
- paperfolding example for trapezoidal words
- period-doubling examples
- Fibonacci examples

- 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 here.
- 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**(2016), 39-66. E-version: here. - Adam Borchert and Narad Rampersad,
Words with many
palindrome pair factors, Arxiv preprint
arXiv:1509.05396 [math.CO], September 17 2015.
Published version in
*Electronic J. Combinatorics***22**(4) (2015), Paper P4.23. - Daniel Goc, Hamoon Mousavi, Luke Schaeffer, Jeffrey Shallit,
A New Approach to the Paperfolding Sequences,
in Arnold Beckmann, Victor Mitrana, Mariya Soskova, eds.,
*Evolving Computability: 11th Conference on Computability in Europe, CiE 2015*, Springer, LNICS, Vol. 9136, 2015, pp. 34-43. Available here. - H. Mousavi and J. Shallit,
Mechanical Proofs of Properties of the Tribonacci Word,
in
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
paper:
- predicates
- TR.txt, put in the "Word Automata" library

- 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.