This companion page for the paper Bounded rewriting induction for LCSTRSs explains how to use Cora to prove equations using bounded rewriting induction.
You can either download and install Cora from source, or using the pre-compiled Java classes supplied on this page. Note that we currently only support UNIX-like systems. So, you can build and run Cora on Linux or MacOS (including M series macs), but Windows is not supported.
The most recent version of Cora can be found at https://github.com/hezzel/cora. Alternatively, download the source of the version of Cora used in this paper here.
Installation directives are available in README.md, but for the short version:
In case compilation fails, we also provide a pre-compiled version.
Unzip app.zip in a directory of your choice, and navigate to the app/bin/ subdirectory. Test if executing ./app works!
In addition, you should ensure that an SMT-solver is installed in your system, or at least available as a binary. By default, Cora assumes that you have Z3 installed, but other SMT-solvers can be passed through runtime parameters (see below).
Given an input file describing the LCSTRS, you can invoke the interactive equivalence prover through one of the following commands (executed in the directory app/bin/):
Do not forget the -e parameter; without it, Cora will attempt to prove termination rather than launching the interactive equivalence prover.
Some example input files that you can use are:
Do not change the file extension! Cora uses this to determine how to parse the input. (Note that browsers may sometimes add a .txt extension when downloading a file.)
To start, you will be prompted to input the equation you want to prove. Note that, to avoid ambiguity with infix symbols, Cora uses functional notation, so you would for instance use rev(append(xs, ys), nil) = append(rev(ys, nil), rev(xs, nil)) and not rev (append xs ys) nil = append (rev ys nil) (rev xs nil). Constraints are placed after a vertical bar, e.g., G(f, k, x) = H(f, n, m, x) | k = n + m.
Then, you can execute commands. All commands can be listed by typing :help commands. To know the syntax of a given command, you would for instance use :help simplify or :syntax simplify .
The deduction rules work as they are described in the paper, with one exception: the simplify command cannot be used with calculation rules. Instead, use the calc command also described in the paper. (There is also a context command not described in the paper; this command is merely a generalisation of semi-constructor.) Several commands require positions; these are for instance l1.3 (for position 1.3.ε in the left-hand side) or r (for the top position on the right), or r4 (for the fourh argument of the right). Note that the l and r are case-sensitive!
To acquire information, the :rules, :hypotheses, :equations and :ordering commands show, respectively, the set of rules, current set H, current set E (use :equations full to also see the bounding terms) and the ordering requirements that have been imposed so far.
To test if the current set of ordering requirements along with the rules is a terminating term rewriting system, use the :check command. To save the current progress, use :save ⟨filename⟩ .
The undo command allows you to go back a step in the prover process, and the redo command allows you to undo an undo. The auto command seeks to do as many simplication, semi-constructor, delete, eq-delete and disprove steps on the current goal as it can. Note that using undo after auto only undoes one of the steps, not necessarily all of them.
A proof process can be saved (using the :save command), so that one can later restart proving from the savepoint. Loading a file must always be the first action: instead of an equation to be proved, simply input the path of the file.
We have provided a full proof for the example inputs, which can be downloaded below. To see a human-readable version of the proof, just load the LCSTRS and the proof file, and then type :check to do the termination check. (In our tests, the termination requirements for all files were immediately proved using the SMT-solver yices.)