fCube, a Prolog theorem prover for Intuitionistic propositional logic based on a
tableau calculus. fCube outputs a proof or a counter model. The main novelty of
fCube is that it implements several optimization techniques that allow to prune the
search space acting on different aspects of the proof-search. In 2010 fCube
outperformed the known provers on several interesting families of formulas.
fCube 11.1 (April 2014): this version contains
some more optimizations than fCube 4.1 but does not
print neither a Kripke countermodel nor a proof.
fCube 4.1 (October 2013): an improvement of
version 3.0, where nested conjunctions and disjunctions are handled in a row.
fCube 3 (May 2012): an old version of fCube, that
outputs a counter model for unprovable formulas.