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


Download the nbu-1.0.jar file.


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.


$ java -jar nbu-1.0.jar -h

for a detailed description of available options.