**lsj** is a prover for Intuitionistic propositional logic based on the calculi
**LSJ** and **RJ** presented in

M. Ferrari, C. Fiorentini, and G. Fiorino. Contraction-free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models.Journal of Automated Reasoning, 51(2):129-149, 2013. [DOI]

Download the `lsj-1.0.jar` file.

Note

`lsj-1.0.jar` requires Java 1.8 or later. The LaTeX files
generated by the application depend on the packages `tikz`,
`xifthen` and `proof` available at CTAN.

Run the `lsj-1.0.jar` file using the following command:

`$ java -jar lsj-1.0.jar [options] [problem file]`

where *[problem file]* (optional) is the file containing the problem description
and *[options]* is a list of options. If the problem file name is not specified
the *-input* option must be specified.

By default the proof-search is performed using the calculus **LSJ**, to use the
calculus **RJ** you can specify the `-p rj` option.

Run:

`$ java -jar lsj-1.0.jar -h`

for a detailed description of available options.

Formulas must be specified using the following syntax:

```
Syntax of formulas
atoms: Java identifiers
logical: false, & (and), | (or), ~ (not), -> (implies), <=> (iff)
notes: (A <=> B) is translated as ((A -> B) & (B -> A))
```

A **problem description** is a file describing an input problem. It
contains the formulas describing the problem and, possibly, other
informations as its name and its provability status.

The prover supports three problem descriptions.

A plain problem description is a file consisting of only one line
specifying the formula to prove. To provide such a file as input use
the `-r plain` option. As an example, the following is a plain
specification of the double negation of the tertium-non-datur
principle.

```
~(~(p | ~p))
```

A **JTabWb** problem description is a file having the following
structure:

```
%------------------------
% Formula : name
% Status : provable|unprovable
%------------------------
formula
%------------------------
```

where:

*name*is the name of the formula;*status*specifies if the formula is*provable*or*unprovable*;*formula*is a formula.

To provide such a file as input use the `-r jtw` option.

As an example, the following is the specification of above problem in JTabWb-format:

```
%------------------------
% Formula : double-negation-tertium-non-datur
% Status : provable
%------------------------
~(~(p | ~p))
%------------------------
```

Some problems specified in the JTabWb format are available in
`ipl_examples_jtabwb.zip`.

Running the prover in non-verbose mode, we get a summary describing the essential
facts about the performed proof-search. For example, running **lsj** on the
Intuitionistically unprovable *Scott principle*, we get:

```
$ java -jar lsj-1.0.jar wffs/ipl_examples_jtabwb/scott.jtabwb
Launcher for lsj and rj (unprovability calculus) for IPL
** Reader [jtawb_format]
> Parsing problem... time (ms) [0]
** Problem [Scott], status [UNPROVABLE]
> Building initial node set... time (ms) [112]
** Prover [lsj 1.0 (seq=bsf)]
> Proving...
****************************************************************
** Prover [lsj 1.0 (seq=bsf)]
** Problem [Scott], status [UNPROVABLE], proof-search [FAILURE], test [PASSED]
** Generated nodes [70], restored backtrack-points [3], restored branch-points [17]
** Timings (ms): PS (proof-search) [17], NSC (initial node set) [112], PP (problem parsing) [0]
** Proof time (PS + NSC + PP): (ms) [129]
****************************************************************
```

The first part of the report describes the actions performed the prover (input parsing, initial node set construction, proof-search). When the proof-search terminates the prover provides details about the performed proof search. In particular the second line describes the result of the proof-search on the given input problem:

*status*is the status of the input problelm (`PROVABLE`,`UNPROVABLE`or`UNKNOWN`).*proof-search*is the status of the proof-search (`SUCCESS`or`FAILURE`).*test*is`PASSED`if the status of the formula match the result of the proof-search and`FAILED`otherwise.

The following lines provide details on the prover execution (number of gnerated nodes, restored backtrack-points and restored branch-point) and execution times.

Running the **lsj** prover on the *Scott principle* specifying the
`-p rj` and `-proof` options, the prover performs the proof-search
using the **Rbu** calculus and generates the LaTeX rendering of the
counter-model.

```
$ java -jar lsj-1.0.jar -p rj -model wffs/ipl_examples_jtabwb/scott.jtabwb
Launcher for lsj and rj (unprovability calculus) for IPL
** Reader [jtawb_format]
> Parsing problem... time (ms) [1]
** Problem [Scott], status [UNPROVABLE]
> Building initial node set... time (ms) [112]
** Prover [rj 1.0 (seq=bsf)]
> Proving...
****************************************************************
** Prover [rj 1.0 (seq=bsf)]
** Problem [Scott], status [UNPROVABLE], proof-search [SUCCESS], test [PASSED]
** Generated nodes [852], restored backtrack-points [237], restored branch-points [3]
** Timings (ms): PS (proof-search) [48], NSC (initial node set) [112], PP (problem parsing) [1]
** Proof time (PS + NSC + PP): (ms) [161]
****************************************************************
> Generating model...done.
> Model LaTeX source saved in [model.tex].
```

Read more: *Verbose mode*.