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.
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].
fCube : an efficient prover for intuitionistic propositional logic
C. Fiorentini;
2010
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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2010_lpar.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
204.41 kB
Formato
Adobe PDF
|
204.41 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
