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.