Porgi


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.

Documentation

Porgi is described in the paper Porgi: a Proof-Or-Refutation Generator for Intuitionistic propositional logic.

Obtaining Porgi's Source

Porgi's source consists of a single file, porgi.sml.

Related links


Alley Stoughton (alley.stoughton@icloud.com)