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).