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
orUNKNOWN
). - proof-search is the status of the proof-search (
SUCCESS
orFAILURE
). - test is
PASSED
if the status of the formula match the result of the proof-search andFAILED
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.