Guido Fiorino
Curriculum
Publications
Software

Didattica
2013-2014
2012-2013
2011-2012
2010-2011
2009-2010
2002-2009
Esami
Ricevimento


fCube

fCube, a Prolog theorem prover for Intuitionistic propositional logic based on a tableau calculus. fCube outputs a proof or a counter model. The main novelty of fCube is that it implements several optimization techniques that allow to prune the search space acting on different aspects of the proof-search. In 2010 fCube outperformed the known provers on several interesting families of formulas.

fCube 11.1 (April 2014): this version contains some more optimizations than fCube 4.1 but does not print neither a Kripke countermodel nor a proof.

fCube 4.1 (October 2013): an improvement of version 3.0, where nested conjunctions and disjunctions are handled in a row.

fCube 3 (May 2012): an old version of fCube, that outputs a counter model for unprovable formulas.






Valid HTML 4.01 Transitional Valid CSS!