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