Comment Comment by The_rationalist I am trying to implement a natural language (English) logic checker. It would detect https://en.m.wikipedia.org/wiki/Formal_fallacyHow 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 syllogismsOne 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) parent The_rationalist 7 years ago
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)