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