fCube

fCube: an efficient prover for intuitionistic propositional logic. We present fCube, a theorem prover for intuitionistic propositional logic based on a tableau calculus. The main novelty of fCube is that it implements several optimization techniques that allow to prune the search space acting on different aspects of 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element