Intuitionistic Propositional Logic Tableaux in Haskell

We present an implementation in Haskell of a tableau-style proof system for the implication-free fragment of intuitionistic propositional logic, drawing inspiration from a preexisting implementation of classical first-order logic. We also propose a tableau prover for classical propositional logic, obtained via a minor modification of the original one. These two can be used in conjunction to have experimental evidence of Glivenko’s theorem.