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.