Proofs

ben-jose can generate proofs for unsatisfiable formulas. To display them you will need a file system web browser like webfs.

This display system was designed as a debug tool so it needs some steps to be used. Also while running it will show some dialogs. Just click ok to all of them.

To install webfs in Linux Mint just type:

	sudo apt-get install webfs

Assuming the program ''bj-batch-solver'' is in the path, and from the source tree directory:

Due to a bug in the last solver version you must first edit the file 'dbg_ben_jose.conf' and uncomment (delete the leading '//') in the line that starts with '//115' so that you can see the paths that you will need later.

	cd ben-jose-master/src/programs/tests/solver
	sh clean_sh
	bj-solver-debug ./h4.cnf -proof -root .
	webfsd -F -p 3000

And from another terminal:

	firefox http://localhost:3000/SKELETON/CNF/Show_Proof.htm &

The expected output can be found in this link.

the bj-batch-solver program will use the bjp_write_proofs library option to generate the proof of the unsatisfiable instance ''h4.cnf'' in JSON format.

Then:

Copy the (very long) path printed in the standard output under "FINAL_PROOF_JSN=" to the text area field in the Show_Proof.htm HTML page. (This will NOT be displayed in stdout if you did not uncomment the line starting with '//115' in the 'dbg_ben_jose.conf' file).
Paths must begin with ''/SKELETON'', so get rid of the prefix before it.
Click ''LOAD\_FILE''