Proof playground

Enter an NJ proof and I'll tell you some things about it!

Input proof:
Output proof:
How to enter a proof:
  • You can input connectives by using the symbols below or their ASCII approximations as shown:
    Connective Write (click to copy symbol to your clipboard):
    Negation
    Conjunction
    Disjunction
    Implication
    Falsum
  • For rule labels, use the connective plus I for introductions or E for eliminations. For disjunction introductions and conjunction eliminations, you should add in addition an L or R as appropriate. For example, you might write ∧I or ∧EL.
  • For discharging rules (that's →I, ¬I, and ∨E), add a numeral to the end of the rule name as a discharge marker. For example, you might use →I5 or ∨E23.
  • To discharge an assumption, surround it with [ and ], and put the appropriate discharge numeral immediately after that. For example, you might write [p -> q]3 to discharge the assumption p -> q with the label 3.
  • Press Enter to create a new sibling node.
  • Press Ctrl-Enter to create a new parent node.
  • Press Ctrl-Shift-Enter to create a new child node.
  • Cycle nodes with Tab and Shift-Tab.
  • Undo and Redo changes with Ctrl-Z and Ctrl-Shift-Z.
  • Delete subtrees with Ctrl-Backspace.
  • Cut, Copy, and Paste subtrees with Shift-Ctrl-X, Shift-Ctrl-C, and Shift-Ctrl-V
  • Finally, if you run into bugs or difficulties, please let me know! Screenshots are very much appreciated.