/LCF-style-ND

Exposition of an LCF-style theorem prover for propositional logic in a Natural Deduction system