I am trying to implement a natural language (English) logic checker. It would detect https://en.m.wikipedia.org/wiki/Formal_fallacy

How could a SAT/SMT help me in this task? I know it's already used for math theorem checking.

E.g All men are mortal. Socrates is a man. Therefore Socrate is mortal. I have currently two way to solve syllogisms

One hard-coded Disjonction of cases (but not flexible enough for non canonical forms of syllogisms)

And a flexible one that generate a graph of transitivity.

Both are 100% accurate.

Could SAT/SMT give me a third way of determining if the conclusion is logically valid? (not non sequitur)