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.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: fCube: an efficient prover for intuitionistic propositional logic (2010)