nbu¶

nbu is a prover for Intuitionistic propositional logic based on a natural deduction calculus

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.