This is a sequent-style prover for propositional intuitionistic logic using a contraction-free calculus

which requires no loop-check.

Roy Dyckhoff

Contraction-Free Sequent Calculi for Intuitionistic Logic.

J. Symb. Log. 57(3): 795-807 (1992)

This is a sequent-style prover for propositional intuitionistic logic using a contraction-free calculus

which requires no loop-check.

Roy Dyckhoff

Contraction-Free Sequent Calculi for Intuitionistic Logic.

J. Symb. Log. 57(3): 795-807 (1992)