Software

The frj prover

The prover frj is a JTabWb implementation of the forward calculus FRJ(G) for Intuitionistic unprovability. This prover was originally presented in

C. Fiorentini and M. Ferrari. A Forward Unprovability Calculus for Intuitionistic Propositional Logic. In R. A. Schmidt and C. Nalon, editors, TABLEAUX 2017, LNCS, vol. 10501, pages 114–130. Springer International Publishing, 2017. [DOI]

The current version allows the user to extract a direct proof of the goal G in the GBU-calculus for intuitionistic provability from the saturated database generated by failed proof-search in FRJ(G).

The prover is available at github.com/ferram/jtabwb_provers/ipl_frj.

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.