# 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]

## Running the prover¶

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.

## Specifying input¶

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

### Problem description¶

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.

#### Plain problem description¶

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

#### JTabWb problem description¶

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`

.

## Output explanation¶

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.