FCube-4.1 for Intuitionistic Propositional Logic

2022-09-04, updated 2022-09-05 next - previous

Ferrari, Fiorentini and Fiorino made fCube i.e. \(F^{3}\).

1. FCube-4.1 verbose version

  • This is version 4.1 of FCube-verbose for Tau Prolog (see this discussion), a prover which provides proofs for intuitionistically valid formulas, and countermodels for those that are intuitionistically unprovable.
  • I changed the code to use infix notation.
  • For the description of FCube algorithm, see [1], [2], below.

    Enjoy !

A - Prolog Code:

D - Examples of Queries:

  1. Excluded Middle: a | ~ a
  2. Dilemma : ((~ a => b) & (a => b)) => b
  3. Double Negation: ~(~a) <=> a
  4. Peirce’s Law: (((a => b) => a) => a)
  5. Dummett Formula : (a => b)| (b => a)
  6. Classical equivalence for negation : (~a => a) <=> a
  7. Classical De Morgan's Law : ~((a & b)) => (~ a | ~b)
  8. Pelletier Problem 17 : ( ( ( p & ( q => r ) ) => s ) <=> ( ( ~ p | q | s ) & ( ~ p | ~ r | s ) ) )
  9. a
  10. a => b
  11. (a | b) => (a & b)

2. References

1.
Ferrari, M., Fiorentini, C., Fiorino, G. Towards the use of Simplification Rules in Intuitionistic Tableaux. In: Atti del convegno CILC09 - 24-esimo Convegno Italiano di Logica Computazionale, 2009, 148–159, [Online]. Available: https://www.vidal-rosset.net/pdf/ferrari2009.pdf.
2.
Ferrari, M., Fiorentini, C., Fiorino, G. FCube: An Efficient Prover for Intuitionistic Propositional Logic. In: Logic for Programming, Artificial Intelligence, and Reasoning, 2010, 294–301, [Online]. Available: https://www.vidal-rosset.net/pdf/ferrarietal2010.pdf.
 

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