FCube: An Efficient Prover for Intuitionistic Propositional Logic
2022-01-11, updated 2022-06-14 next - previous
Ferrari, Fiorentini and Fiorino made fCube i.e. \(F^{3}\).
1. FCube Prover Online
- FCube prover online is version 4.1 of FCube-verbose, which provides proofs for intuitionistically valid formulas, and countermodels for those that are intuitionistically unprovable.
- I only changed the code 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.
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.
