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 -p asks mjc to prove all the formulas defined in (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).