swMATH ID: 11383
Software Authors: Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido
Description: 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.
Homepage: http://www2.disco.unimib.it/fiorino/fcube.html
Related Software: ILTP; Imogen; IntHistGC; JTabWb; DeReS; MiniSat; intuit; Isabelle; Cool; MetTeL; LoTREC; CoLoSS; PVS; BDDIntKt; BuDDy
Cited in: 10 Publications

Citations by Year