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.
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
2010
Book Part (author)
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/148078
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 21
  • ???jsp.display-item.citation.isi??? 15
social impact