Walnut documentation - Walnut-Theorem-Prover/Walnut GitHub Wiki

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.

The Walnut book also contains hundreds of applications of Walnut to various problems, with code you can paste in verbatim and run. The first edition uses the earlier Walnut 3.7.

Additionally, each version has its own documentation:

• Walnut 7 - improved speed and memory usage, Sessions, automata trimming, Metacommands (including OTF)

  • CHANGELOG
  • Using the strategy metacommand This is used to choose different determinization strategies such as OTF

• Walnut 6 - 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 - support for the Ostrowski numeration systems; detailed description of Ostrowski enhancement