1. Using Walnut - Walnut-Theorem-Prover/Walnut GitHub Wiki

Walnut 7 requires JDK 17 or higher.

Run build.sh to build. You can run all of the tests by running build.sh -t.

walnut.sh is used to run Walnut.

Usage: walnut [OPTIONS] [<filename>]

Walnut command-line interface.

Positional arguments:
  <filename>          File of commands to execute (same effect as the `load`
                      command). If omitted, starts an interactive session.

Options:
  --global-session    Use the old (Walnut 6 or earlier) global session behavior.
  --session-dir PATH  Use PATH instead of an auto-generated Session directory.
  --home-dir PATH     Use PATH instead of the current working directory.
  --help              Show this help message and exit.

To invoke Walnut with more memory, see the walnut.sh file; change it appropriately for your system resources.

Walnut 7 introduces the concept of Sessions. These allow users to logically organize their Walnut experiments, and not be concerned with overwriting old ones.

Previous versions of Walnut only had the concept of a global session. (If you prefer this behavior, run "walnut.sh --global-session".)

By default, Walnut creates a new Session directory on every run (e.g., Session/2025_10_30_15_34/), which is where new files are written.

Optionally, the user can specify an older Session directory (e.g., "walnut --session-dir=Session/2024_10_30_12_00/"), to continue working with a previous experiment.

Some advice can be found in the Walnut book, but additionally:

• Remove trivial/vacuous statements or variables. e.g.:
  • x >= 0 is always true
• Consider "weakening", e.g.:
  • Instead of Ax f(x) & g(x), prove Ax f(x) and Ax g(x) separately
• Reformulating queries can help
  • def tribfaceq "?msd_trib At (t<n) => TR[i+t]=TR[j+t]": is much slower than def tribfaceq2 "?msd_trib Ax Ay (x>=i & x<i+n & x+j=y+i) => TR[x]=TR[y]":
  • Note that different determinization algorithms are faster here
• Au,v f(u,v) => g(u,v) can be written instead as ~Eu,v f(u,v) & ~g(u,v), which can be much faster due to totalization (pointed out by Nicolas Ollinger)
• Try a different determinization algorithm: see the [strategy] metacommand

Every command ends in either a colon, double colon, or a semicolon. Semicolon gives the least details on intermediate steps of computations, whereas double colon gives the most. (Metacommands, which work on intermediate steps, require double colon to be used.)

For example, typing: def sample "a = b + 1" : gives output similar to this:

a=(b+1) : 2 states − 1ms
Total computation time : 4ms.

This shows that the automaton for the predicate a = b + 1 has 2 states and took 4 milliseconds to compute.

When a single colon is used, Walnut prints only the major steps of a computation. Use two colons if you want to see all the steps (cross product, quantification, fixing leading zeros, trimming, NFA and DFA minimization, determinization, etc.): def sample "a = b + 1" :: gives output similar to this:

computing b+1
computed b+1
computing a=(b+1)
 computing &:1 states - 2 states
  computing cross product:1 states - 2 states
  computed cross product:2 states - 7ms
  Minimizing: 2 states.
  Minimized:2 states - 0ms.
 computed &:2 states - 7ms
 quantifying:2 states
   Determinizing [#0, strategy: SC]: 2 states
   Determinized: 2 states - 3ms
   Minimizing: 2 states.
   Minimized:2 states - 1ms.
 quantified:2 states - 4ms
 fixing leading zeros:2 states
  Determinizing [#1, strategy: SC]: 2 states
  Determinized: 2 states - 0ms
  Minimizing: 2 states.
  Minimized:2 states - 0ms.
 fixed leading zeros:2 states - 0ms
computed a=(b+1)
a=(b+1):2 states - 11ms
Total computation time: 13ms.

Whitespace is ignored. Thus you can split a command into multiple lines to improve readability. All of these are equivalent:

def sample "a = b + 1";

def sample
"a  =b   + 1"  ;

def sample
"a=b+1"
;

We must separate the name and predicate, otherwise Walnut will return an error: def sample"a = b + 1" ; yields Invalid use of the eval/def command.

For details about individual commands, please see: Walnut commands reference