Home - Walnut-Theorem-Prover/Walnut GitHub Wiki
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
- This includes the Walnut commands reference
Other Documentation for Walnut
Developing Walnut
- A detailed description of the Walnut file format
- Other supported file formats (BA, Graphviz, and several matrix formats)