, a theorem prover for Intuitionistic propositional logic based on a tableau calculus. The main novelty of
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
with other theorem provers. We found that our prover outperforms the other provers on several interesting families of formulas.