Name
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-16242-8_21 | LPAR (Yogyakarta) |
Keywords | Field | DocType |
different aspect,optimization technique,theorem provers,main novelty,interesting family,search space,tableau calculus,efficient prover,intuitionistic propositional logic,theorem prover,propositional logic | Theorem provers,Discrete mathematics,Computer science,Automated theorem proving,Propositional calculus,Algorithm,Theoretical computer science,Novelty,Gas meter prover,Propositional variable | Conference |
Volume | ISSN | ISBN |
6397 | 0302-9743 | 3-642-16241-X |
Citations | PageRank | References |
13 | 0.85 | 9 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mauro Ferrari | 1 | 93 | 16.05 |
| Camillo Fiorentini | 2 | 121 | 21.00 |
| Guido Fiorino | 3 | 97 | 12.71 |