In this system description we provide FCUBE, a theorem prover for Intuitionistic propositional logic based on a tableau calculus. The main novelty of cube is that it implements several optimization techniques that allow to prune the search space acting on different aspects of the 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

FERRARI, MAURO;FIORENTINI, CAMILLO;FIORINO, GUIDO
2010-01-01

Abstract

In this system description we provide FCUBE, a theorem prover for Intuitionistic propositional logic based on a tableau calculus. The main novelty of cube is that it implements several optimization techniques that allow to prune the search space acting on different aspects of the 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.
2010
Fermüller C. G., Voronkov A.
Logic for Programming, Artificial Intelligence, and Reasoning, 17th International Conference, LPAR-17
9783642162411
Logic for Programming, Artificial Intelligence, and Reasoning 17th International Conference, LPAR-17
Yogyakarta
October 10-15, 2010
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11383/1718641
 Attenzione

L'Ateneo sottopone a validazione solo i file PDF allegati

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 16
social impact