Publication Date:
2010
Citation:
fCube : an efficient prover for intuitionistic propositional logic / M. Ferrari, C. Fiorentini, G. Fiorino - In: Logic for programming, artificial intelligence, and reasoning : 17th international conference, LPAR-17 : Yogyakarta, Indonesia, october 10-15, 2010 : proceedings / [a cura di] C.G. Fermüller, A. Voronkov. - Berlin : Springer, 2010. - ISBN 9783642162411. - pp. 294-301 (( Intervento presentato al 17th. convegno International Conference on Logic for Programming, Artificial Intelligence and Reasoning tenutosi a Yogyakarta, Indonesia nel 2010 [10.1007/978-3-642-16242-8_21].
abstract:
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.
IRIS type:
03 - Contributo in volume
List of contributors:
M. Ferrari, C. Fiorentini, G. Fiorino
Link to information sheet:
Book title:
Logic for programming, artificial intelligence, and reasoning : 17th international conference, LPAR-17 : Yogyakarta, Indonesia, october 10-15, 2010 : proceedings