nbu¶
nbu is a prover for Intuitionistic propositional logic based on a natural deduction calculus
Download¶
Download the nbu-1.0.jar
file.
Note
nbu-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 nbu-1.0.jar
file using the following command:
$ java -jar nbu-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 -i option must be specified.
Run:
$ java -jar nbu-1.0.jar -h
for a detailed description of available options.