# Software¶

## The **mjc** prover¶

The prover **mjc** is a Prolog prototype implementing the
proof-search procedures presented in the paper:

M. Ferrari, C. Fiorentini.Proof-search in Classical Propositional Natural Deduction via an Isomorphic Sequent Calculus

Given a propositional formula F:

- if F is provable in Classical propositional logic, then
**mjc**yields a latex file containing a derivation of F in the calculus**MJcr**, its translation in**MJc**and the corresponding natural deduction derivation in**NC**. - Otherwise,
**mjc**shows an interpretation falsifying F.

The source files are available in `mjc.tar`

(see the file `README.txt`

for the usage
instructions).

The command line `mjc.sh -p`

asks **mjc** to prove all the formulas
defined in `test.pl`

(the default test file) and to generate the
`latex`

and `pdf`

files containing the derivations of provable
formulas.

The obtained latex files are in `examples.tar`

.

The corresponding `pdf`

files are gathered in `examples.pdf`

(note that the derivations are very
tiny and must be magnified).

**JTabWb**¶

**JTabWb** is a Java framework for developing provers based on
terminating sequent or tableau calculi. It can be used either to
implement provers as stand-alone Java applications or as APIs to be
integrated in Java applications.

The framework provides support for generation of proof-traces (histories of proof-search), LaTeX rendering of proofs and counter-model generation.

### Download¶

**JTabWb** requires Java 1.8 or later. Download the
`jtabwb-1.0.jar`

file and add
it to your CLASSPATH. You can browse the API
or download the tarball file `jtabwb-1.0-apidocs.zip`

.

Sources, binaries and documentation are available at github.com/ferram/jtabwb

## Provers implemented in **JTabWb**¶

Here we describes some of the provers we have implemented in **JTabWb**,
other provers are available at github.com/ferram/jtabwb_provers

### clnat¶

clnat is a prover for *Classical propositional
logic* based on the natural deduction calculus **Ncr** presented in

M. Ferrari and C. Fiorentini. Proof-search in natural deduction calculus for classical propositional logic. In H. De Nivelle, editor,TABLEAUX 2015, LNCS, vol. 9323, pages 237–252. Springer International Publishing, 2015. [DOI]

### g3ibu¶

g3ibu is a prover for *intuitionistic propositional logic* based on the sequent
calculi **Gbu** and **Rbu** presented in

M. Ferrari, C. Fiorentini, and G. Fiorino. A terminating evaluation-driven variant of G3i. In D. Galmiche and D. Larchey-Wendling, editors,TABLEAUX 2013, LNCS, volume 8123, pages 104-118. Springer-Verlag, 2013. [DOI]

### g3ied and rg3ied¶

g3ied is a prover for *intuitionistic propositional logic*
implementing the evaluation driven proof-search procedure for **G3i** presented
in

M. Ferrari, C. Fiorentini, and G. Fiorino. An Evaluation-Driven Decision Procedure for G3i.ACM Transactions on Computational Logic (TOCL), 6(1):8:1–8:37, 2015. [DOI]

### 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]

## FCube¶

FCube is the theorem prover for *intuitionistic propositional logic* described in

M. Ferrari, C. Fiorentini, and G. Fiorino. FCube: An Efficient Prover for Intuitionistic Propositional Logic. In C. G. Fermuller and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17, volume 6397, pages 294-301. Springer, 2010. [DOI]

FCube is based on a tableau calculus and it implements some of the optimization techniques descibed in

M. Ferrari, C. Fiorentini, and G. Fiorino. Simplification Rules for Intuitionistic Propositional Tableaux.ACM Transactions on Computational Logic (TOCL), 13(2), 2012. [DOI]

Fcube is written in SWI-Prolog.