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.