The top block gives some premises and a conclusion which we're meant to prove. The smaller blocks on the bottom are inference rules which can be used in the proof. I haven't figured out what the colors mean. I think there's also some kind of cursor/state, which I don't understand -- but when you click a rule, I don't understand how you control which expression matches to which term in the rule.
[+] [-] techtangents2|2 years ago|reply
[+] [-] mcphage|2 years ago|reply
[+] [-] abeppu|2 years ago|reply