I've thought a bit about a game like this in the past and came to the conclusion that UI would be a nightmare. It's might be manageable as long as you stick to propositional calculus, but it's pretty limited and if you try to go further then substitution rules for quantifiers come into play. Maybe there is a way to make it work, but I don't think it's something you can just walk into without some consideration.