The sequent checker responds with error messages that make sense describing sequent calculus proofs, but not truth-trees, usually"This doesn't follow by this rule" or "wrong number of premises".
We should map the errors from the sequent checker to something that makes more sense in our context.
The sequent checker responds with error messages that make sense describing sequent calculus proofs, but not truth-trees, usually"This doesn't follow by this rule" or "wrong number of premises". We should map the errors from the sequent checker to something that makes more sense in our context.