I have recently seen in Lambda the Ultimate an announcement for an interactive tutorial on first order logic. It is really nice to visually see the application of the logic rules, as well as proving things (aka get the proof obligation get green) just by clicking.

With such an interface, proof is like a game! :-)