WALNUT SOFTWARE

What is Walnut?

Walnut is free software, written in Java, for deciding first-order statements about the non-negative integers, phrased in an extension of Presburger arithmetic, called Buchi arithmetic. It can be used to provide rigorous proofs or disproofs of hundreds of assertions in combinatorics on words, number theory, and other areas of discrete mathematics. It can handle a wide variety of problems, and has been used to disprove false claims in the literature, as well as solve open problems.

Where can I learn more about Walnut?

You can buy a book, or watch a video about Walnut, or look at some examples of how it can be used. There are also some exercises you can try once you have mastered the basics of Walnut.

Where can I download Walnut?

The current version of Walnut is 6.2, and can be downloaded for free at https://github.com/Walnut-Theorem-Prover.

Where is the documentation about Walnut?

Currently there is no one single document with all of Walnut's features. The base document, about the first version of Walnut (aka Walnut 1), is this arxiv preprint by Hamoon Mousavi, originally written in 2016 and updated in 2021. Since then, many new features have been added to Walnut:

Walnut 6 (the current version; improved speed and memory usage, added basic automaton operations)
Walnut 5 (support for transducers)
Walnut 4 (support for queries over Z instead of N)
Walnut 3 (provides regular expressions for k-tuples of strings; combine DFA's into a DFAO; convert uniform morphism to a DFAO, etc.)
Walnut 2 (provides support for the Ostrowski numeration systems)

The Walnut book also contains literally dozens and dozens of applications of Walnut to various problems, with code you can just paste in verbatim and run.

How do I install Walnut?

See this page.

I don't want to install it, can I just try it out in a web interface?

Yes! Thanks to Nicolas Ollinger, you can go to this URL. It takes about 15-30 seconds to load. Once it loads, click the button that says "New ▼" and select "Walnut". You will now see a green rectangle. You can now type in Walnut commands and click "▶ Run" to execute them. Try, for example

def tm_has_overlap "Ei,n n>=1 & At (t<=n) => T[i+t]=T[i+n+t]":

which is Walnut's way of writing the first-order logic assertion

∃ i, n n ≥ 1 and ∀ t (t ≤ n) ⇒ t_i+t = t_i+n+t .

This expression/Walnut command asserts that the Thue-Morse sequence t = 011010011001 … has an overlap. (An overlap is a block of the form axaxa, where a is a single letter, and x is a (possibly empty) word.)

Now Walnut returns FALSE, so this constitutes a rigorous proof that t has no overlaps.

How can I report bugs or complain about issues?

Go to this web page. You might have to register for github.

Where are older versions of Walnut?

Where can I read papers about using Walnut to solve problems?

This page has a list of over 100 papers, books, and theses that have used Walnut in some way to prove results in number theory, combinatorics on words, and other fields of discrete mathematics.

Who are the developers of Walnut?

The principal architect of Walnut 1 was Hamoon Mousavi. Aseem Baranwal added features to Walnut 2. Laindon C. Burnett added features to Walnut 3. Kai Hsiang Yang added features to Walnut 4. Anatoly Zavyalov added features to Walnut 5. Anatoly Zavyalov added features to Walnut 6, and John Nicol rewrote large portions of the code to significantly improve speed and memory usage. Walnut 7 development is currently underway by John Nicol. Jeffrey Shallit contributed ideas to the development of Walnut versions 1 through 6, but no actual programming.