Software for teaching logic

I realise this is slightly off topic, but I am keen to find out
what `types people' use for teaching logic to computing undergraduates.

In particular, I am looking for feedback on systems which allow
students to build proofs (preferably in a natural deduction style) in 
propositional and predicate logic. The best thing would be to reply
directly to me, and I will post a summary of responses to the types list.

Thanks very much,

Simon Thompson