Data di Pubblicazione:
2010
Citazione:
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.
Tipologia IRIS:
03 - Contributo in volume
Elenco autori:
M. Ferrari, C. Fiorentini, G. Fiorino
Link alla scheda completa:
Link al Full Text:
Titolo del libro:
Logic for programming, artificial intelligence, and reasoning : 17th international conference, LPAR-17 : Yogyakarta, Indonesia, october 10-15, 2010 : proceedings