Walnut

Automatic Theorem Prover for Automatic Words

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 download Walnut?

The latest version of Walnut can be downloaded for free at https://github.com/Walnut-Theorem-Prover.

Where is the documentation about Walnut?

Please see the Walnut wiki for the most up-to-date documentation about Walnut!

To learn even more about Walnut, see Jeff's Walnut page. There are links to his book, videos, and more Walnut examples and exercises there once you have mastered the basics of Walnut.

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

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 blue rectangle. You can now type in Walnut commands and click on the small black right-pointing triangle ▸ to run them. Try, for example

eval tm_has_overlap "Ei,n n>=1 & Aj (j<=n) => T[i+j]=T[i+n+j]":

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

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

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.

To see an automaton, use the command
%showme name
where name is replaced by the name of the automaton you want to see.

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 was by John Nicol. Jeffrey Shallit contributed ideas to the development of Walnut versions 1 through 7, but no actual programming.