This is the abstract of technical report TR-ARP-12-94 ( dvi or postscript)
The program minlog is a theorem prover for propositional minimal and intuitionist logic, based on a cut-free sequent calculus. It achieves speed more through careful coding than by incorporating sophisticated logical techniques. It makes use of certain extra (derivable) rules to shorten proofs in trivial ways, and it avoids some searching by not working on the same sequent twice during the same proof search and by not trying to prove sequents which are not classical tautologies. Proofs may be displayed in a Fitch-style natural deduction format.
As well as being a tool for the logical investigation of constructive systems, minlog is put forward as representing the baseline for high performance theorem proving in this area.
The program), with sources, Makefile, documentation and `man' page, is available by anonymous ftp.