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