FCube: An Efficient Prover for Intuitionistic Propositional Logic

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

  • This version 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 of the prover below, see [1].
  • Syntax for input formulas: ~a , a & b, a | b ,a =>b , a <=> b (for, respectively, negation, conjunction, disjunction, conditional and biconditional .
  • Choose a formula in the list below, or input your one
Either an intuitionistic proof or an intuitionistic refutation will be given 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.

orgmode emacs isso debian mxlinux