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