Porgi is a Proof-Or-Refutation Generator for Intuitionistic propositional logic. Given a sequent, Porgi either finds a minimally sized, normal natural deduction of the sequent, or it finds a "small", tree-based Kripke countermodel of the sequent.
Porgi is written in Standard ML, and is intended to be compiled using MLton, producing an executable, which can be exectuted from the shell.
Porgi is described in the paper Porgi: a Proof-Or-Refutation Generator for Intuitionistic propositional logic.
Porgi's source consists of a single file, porgi.sml.