# FCube: An Efficient Prover for Intuitionistic Propositional Logic

2021-12-23, updated 2021-12-23 next - previous

Ferrari, Fiorentini and Fiorino made FCube i.e. $$F^{3}$$.

## 1. FCube Prover Online

### 1.2Specifications

• FCube-verbose 4.1 is a SWI-Prolog program that, for any propositional formula should provide either an intuitionistic proof or a Kripke countermodel.
• I changed the code only to use infix notation.
• Mutatis mutandis, the php script is Carlo Capelli’s, on which runs Boole-Quine prover.
• For the description of FCube algorithm, see [1] below.

### 1.3Syntax

For respectively, negation, conjunction, disjunction, conditional and biconditional:

 ~a a & b a | b a => b a <=> b
Either an intuitionistic proof or an intuitionistic  refutation will show here

## 2. References

[1]
Ferrari, M. et al.: FCube: An Efficient Prover for Intuitionistic Propositional Logic. In: Logic for programming, artificial intelligence, and reasoning (Editors: C. G. Fermüller and A. Voronkov). Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, p. 294–301.

Made with Emacs 29.0.50 (Org mode 9.5) and with org-export-head, a blog exporter.

The css file of this blog is mainly the result of Zhitao Gong's work.