# lsj¶

**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¶

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.

## Running the prover¶

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 `-ref`

option.

Run:

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

for a detailed description of available options.

Read more about Input specification and Launcher output explanation.