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]

nbu

nbu is a prover for intuitionistic propositional logic based on a natural deduction calculus.

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.

Previous topic

The mjc prover