> So how can I compare the multiline Hs->~Ms with a ~(Hs->Ms) that has the same newline behavior?

I was wondering about that, too, but I could only figure out putting it all on one line.

> Is this syntax based on the syntax used in some scientific field?

I think the quantifier notation is vaguely Peano's original notation, and I think the idea of having HYPOTHESES -> CONCLUSIONS is sort of a Coq-like "above-the-line and below-the-line" thing, or maybe it's that way because it's optimized for syllogisms. Other than that, I've never seen a logic language quite like this one before.

Something I'd like to see someday is a Scratch-like snap-together logic and proof language. I toyed with the idea when I was teaching a discrete math course, but I didn't have time to develop one.