News

December 2 2022

The Walnut book is now available from Cambridge University Press. Get your copy today!

August 15 2022

Walnut 4 is now available! It contains several new and useful commands, in particular for handling negative bases and quantification over Z instead of N.

It is available for download here. This version incorporates new original work by Kai Hsiang Yang.

September 6 2021

Walnut 3 is now available! It contains several new and useful commands. It is available for download here. This version represents additional work done by Laindon C. Burnett to the previous versions of Walnut written by Hamoon Mousavi and updated by Aseem Raj Baranwal. For this version, you should type java Main.Prover to get started, insted of the older java Main.prover.

Installing Walnut

When you go to the github site above, click on the green "Code" button, then choose "Download Zip".

When you get the zip file downloaded, you might (depending exactly one what system you use) just click on it to extract it. Otherwise you might have to use a zip extractor.

Now you should have a directory called something like Walnut-main.

Go into that directory and there is a command called "build.sh".

Execute that command - on my system you type

./build.sh

to do that.

That should take a few seconds to compile.

Then go to the "bin" directory and type

java Main.Prover

that gets you into Walnut. To leave, type quit;

Depending on your system, you may need a "Java Development Kit" to install Walnut. If so, try the command

sudo apt install openjdk-11-jdk

from a terminal window. Once that is done, to compile Walnut, go to the Walnut directory and type

sh build-sh (Windows)

or

./build-sh (Linux)

That should do it! Now you are ready to go to the "bin" directory and type

java Main.Prover

Let me know if you have any difficulties.

Walnut Software

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 of problems. There are some recent additions to Walnut, written by Aseem Baranwal.

The old version of Walnut is available at github. For the new version, see above. 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:

Here is a talk, given on October 18 2022, about how to use Walnut to prove properties of the sequences in the OEIS:

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 or 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 and books. A partial list is here (will be updated):

  1. Jeffrey Shallit, Proof of a conjecture of Krawchuk and Rampersad, arxiv preprint arXiv:2301.11473 [math.CO], January 27 2023. Available at https://arxiv.org/abs/2301.11473.
  2. Jeffrey Shallit, Counterexample to a Conjecture of Dombi in Additive Number Theory, Arxiv preprint arXiv:2212.12473 [math.NT], December 23 2022.
  3. Dominik Leon Jilg, Frobeniuszahl ausgewählter Zahlenfolgen: Analyse der Frobeniuszahl von synchronisierten Folgen und Folgen mit automatisierter charakteristischer Folge, Bachelor's thesis, Lehrstuhl für Mathematik IV, Julius-Maximilians-Universität Würzburg, Germany, August 12 2022.
  4. Jeffrey Shallit, The Logical Approach To Automatic Sequences: Exploring Combinatorics on Words with Walnut, London Math. Soc. Lecture Note Series, Vol. 482, Cambridge University Press, September 29 2022.
  5. Rob Burns, The appearance function for paper-folding words, arxiv preprint arXiv:2210.14719 [math.NT], October 22 2022.
  6. Jeffrey Shallit, Some Tribonacci conjectures, arxiv preprint arXiv:2210.03996 [math.CO], October 8 2022. Here are the files for the automata you will need in this paper. Put them in the "Automaton Library" of Walnut.
  7. Aseem Baranwal, James Currie, Lucas Mol, Pascal Ochem, Narad Rampersad, and Jeffrey Shallit, Antisquares and critical exponents, arxiv preprint arXiv:2209.09223 [math.CO], September 19 2022.
  8. Luke Schaeffer and Jeffrey Shallit, The First-Order Theory of Binary Overlap-Free Words is Decidable, arxiv preprint arXiv:2209.03266 [cs.FL], September 7 2022.
  9. Jeffrey Shallit, Sonja Linghui Shan, and Kai Hsiang Yang, Automatic Sequences in Negative Bases and Proofs of Some Conjectures of Shevelev, arxiv preprint arXiv:2208.06025 [cs.FL], August 11 2022, available at https://arxiv.org/abs/2208.06025.
  10. Joseph Meleshko, Pascal Ochem, Jeffrey Shallit, and Sonja Linghui Shan, Pseudoperiodic words and a question of Shevelev, Arxiv preprint, July 21 2022, http://arxiv.org/abs/2207.10171 .
  11. Shuo Li, A note on the Lie complexity and beyond, Arxiv preprint arXiv:2207.05859 [math.CO], July 12 2022, available at https://arxiv.org/abs/2207.05859.
  12. Golnaz Badkobeh, Tero Harju, Pascal Ochem, and Matthieu Rosenfeld, Avoiding square-free words on free groups, Theoretical Computer Science 922 (2022) 206-217.
  13. James Currie, Pascal Ochem, Narad Rampersad, and Jeffrey Shallit, Properties of a ternary infinite word. Arxiv preprint arXiv:2206.01776 [cs.DM], June 3 2022. Available at https://arxiv.org/abs/2206.01776. To reproduce the calculations, first download the latest version of Walnut here. Second, put the two files in the Custom Bases directory. Third, put the file in the Word Automata directory. Fourth, put the files in the Automata Library directory. Finally, all the commands from the paper are in the file

  14. R. Burns, Factorials and Legendre's three-square theorem: II, arxiv preprint arXiv:2203.16469 [math.NT], March 30 2022. Available at https://arxiv.org/abs/2203.16469.
  15. J. Shallit, Note on a Fibonacci parity sequence, arxiv preprint arXiv:2203.10504 [cs.FL], March 20 2022. Available at https://arxiv.org/abs/2203.10504.
  16. N. Rampersad, The periodic complexity function of the Thue-Morse word, the Rudin-Shapiro word, and the period-doubling word, arxiv preprint arXiv:2112.04416, December 8 2021. Available at https://arxiv.org/abs/2112.04416.
  17. N. Rampersad, Prefixes of the Fibonacci word that end with a cube, arxiv preprint arXiv:2111.09253, November 17 2021. Available at https://arxiv.org/abs/2111.09253.
  18. J. Shallit, Intertwining of Complementary Thue-Morse Factors, arxiv preprint arXiv:2203.02917 [cs.FL], March 6 2022. Available at https://arxiv.org/abs/2203.02917. Revised, published version in Australasian J. Combinatorics 84 (2022), 419-430. Available here .
  19. J. Shallit, Sumsets of Wythoff sequences, Fibonacci representation, and beyond, Periodica Mathematica Hungarica 84 (2022), 37--46. Available here.
  20. Phakhinkon Napp Phunphayap, Prapanpong Pongsriiam, and Jeffrey Shallit, Sumsets associated with Beatty sequences, to appear, Discrete Mathematics.
  21. John Machacek, Mechanical proving with Walnut for squares and cubes in partial words, arxiv preprint arXiv:2201.05954 [cs.FL], January 16 2022. Appeared in CPM 2022, Leibniz Int'l Proc. Informatics, Vol. 223, 2022, pp.5:1-5:11.
  22. J. Shallit, Additive Number Theory via Automata and Logic, arxiv preprint arXiv:2112.13627 [math.NT], December 27 2021.
  23. G. Fici and J. Shallit, Properties of a Class of Toeplitz Words, arxiv preprint arXiv:2112.12125 [cs.FL], December 23 2021.
  24. C. S. Kaplan and J. Shallit, A frameless 2-coloring of the plane lattice, Math. Magazine 94 (5) (2021), 353-360. A limited number of free-eprints are available here.
  25. N. Rampersad and J. Shallit, Congruence properties of combinatorial sequences via Walnut and the Rowland-Yassawi-Zeilberger automaton, Arxiv preprint arXiv:2110.06244 [math.CO], October 12 2021. Appeared in Elect. J. Combinatorics 29 (3) (2022), P3.36.
  26. J. Shallit, Synchronized sequences, in T. Lecroq and S. Puzynina, eds., WORDS 2021, LNICS 12847, Springer, 2021, pp. 1-19.
  27. Jarkko Peltomäki and Ville Salo, Automatic winning shifts, Arxiv preprint arXiv:2106.07249 [cs.FL], June 14 2021.
  28. J. Shallit, Hilbert's spacefilling curve described by automatic, regular, and synchronized sequences, Arxiv preprint arXiv:2106.01062 [cs.FL], June 2 2021. Files for the Walnut proofs:
  29. Jeffrey Shallit, Frobenius numbers and automatic sequences, Arxiv preprint arXiv:2103.10904 [math.NT], March 19 2021. Files for the paper:
  30. Jason P. Bell and J. Shallit, Lie complexity of words, Arxiv preprint, Feb 7 2021, arXiv:2102.03821 [cs.FL]. Available here.
  31. 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.
  32. Jeffrey Shallit, Robbins and Ardila meet Berstel, Info. Proc. Letters 167 (2021). Available at https://doi.org/10.1016/j.ipl.2020.106081.
  33. 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:
  34. 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:

  35. Jeffrey Shallit, Robbins and Ardila meet Berstel, Arxiv preprint 2007.14930, July 29 2020.
  36. Daniel Gabric and Jeffrey Shallit, The simplest binary word with only three squares, Arxiv preprint 2007.08188, July 17 2020. Data for the paper:
  37. 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.
  38. 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.
  39. Aseem Raj Baranwal, Decision algorithms for Ostrowski-automatic sequences, Master's thesis, University of Waterloo, 2020.
  40. 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.
  41. 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.
  42. 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.
  43. 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.
  44. 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.
  45. James Currie and Narad Rampersad, On some problems of Harju concerning squarefree arithmetic progressions in infinite words, arxiv preprint, December 5 2018.
  46. 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.
  47. Colin Krawchuk and Narad Rampersad, Cyclic Complexity of Some Infinite Words and Generalizations, Integers 18A (2018), #A12.
  48. Jeffrey Shallit and Ramin Zarifi, Circular critical exponents for Thue–Morse factors, RAIRO Info. Theor., published online 17 January 2019. Available here.
  49. 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.
  50. 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.
  51. 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.
  52. 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.
  53. 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.
  54. A. Rajasekaran, N. Rampersad, J. Shallit, Overpals, Underlaps, and Underpals, in WORDS 2017: Combinatorics on Words, 2017, pp. 17-29.
  55. 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" library:

  56. Quentin Valembois, Propriétés décidables des suites automatiques, Master's thesis, University of Liège, Belgium, 2017. Available here.
  57. 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.
  58. 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.
  59. 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.
  60. Floriane Magera, Automatic demonstration of mathematical conjectures, Master's thesis, University of Liège, 2015-6. Available at https://matheo.uliege.be/handle/2268.2/1679.
  61. 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.
  62. 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.
  63. 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:
  64. 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.