2010 | OriginalPaper | Buchkapitel
fCube: An Efficient Prover for Intuitionistic Propositional Logic
verfasst von : Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.