fCube: An Efficient Prover for Intuitionistic Propositional Logic

In this system description we provide FCUBE, a theorem prover for Intuitionistic propositional logic based on a tableau calculus. The main novelty of cube is that it implements several optimization techniques that allow to prune the search space acting on different aspects of the proof-search. We tested the efficiency of our techniques by comparing FCUBE with other theorem provers. We found that our prover outperforms the other provers on several interesting families of formulas.