Home

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.

---

Using Walnut

Using Walnut

• This includes the Walnut commands reference

Other Documentation for Walnut

---

Developing Walnut

Developing Walnut

• A detailed description of the Walnut file format
• Other supported file formats (BA, Graphviz, and several matrix formats)

---

Miscellaneous

• Normalization of expansions in exotic numeration systems

• How Walnut does multiplication by constants

• Notes on Walnut 7 performance for the Frobenius Coin Problem