Some searching found http://logitext.mit.edu/tutorial . It tries to explain sequent calculus with an interactive gui prover. Not sure how approachable it is... I've gotten too used to these things to know how to explain them properly.
No comments yet.