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. © 2010 Springer-Verlag.

Ferrari, M., Fiorentini, C., Fiorino, G. (2010). fCube: An Efficient Prover for Intuitionistic Propositional Logic. In Logic for Programming, Artificial Intelligence, and Reasoning "17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010, Proceedings" (pp.294-301). Berlin : Springer Berlin / Heidelberg [10.1007/978-3-642-16242-8_21].

fCube: An Efficient Prover for Intuitionistic Propositional Logic

FIORINO, GUIDO GIUSEPPE
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. © 2010 Springer-Verlag.
slide + paper
propositional intuitionistic logic; automated theorem proving;
English
Logic for Programming, Artificial Intelligence, and Reasoning
2010
Logic for Programming, Artificial Intelligence, and Reasoning "17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010, Proceedings"
9783642162411
2010
6397
294
301
none
Ferrari, M., Fiorentini, C., Fiorino, G. (2010). fCube: An Efficient Prover for Intuitionistic Propositional Logic. In Logic for Programming, Artificial Intelligence, and Reasoning "17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010, Proceedings" (pp.294-301). Berlin : Springer Berlin / Heidelberg [10.1007/978-3-642-16242-8_21].
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/10281/22203
Citazioni
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 16
Social impact