IPL KE-tableau Prover

Pick a preset or write your own formula in the internal Polish notation (e.g. F ->(-(-A) A) c0). Click Solve to run the prover and view the proof tree, rule instances and trace.
Connectives: -X = ¬X, *(X Y) = X∧Y, +(X Y) = X∨Y, ->(X Y) = X→Y. Labels: c0, c1, …. Sign + formula + label, e.g. F ->(p q) c0. Multi-formula problems: one signed formula per line. Hint: Cmd/Ctrl+Enter submits.