Brian Tackett, a computer science student at the University of Buffalo who previously studied philosophy, has created an “automated modal reasoner.”
The program “takes lists of formalized sentences and checks them for consistency or validity in Propositional Modal Logic (S5 Axiom System).” He notes: “Since modal logic extends non-modal logic, this program can also be used for non-modal propositional logic.” However, “Quantifiers like ‘all’ and ‘some’ are not supported at this time.”
I asked him about why he made the program. He replied:
Mainly, I wanted to see how difficult it would be to program a computer to analyze arguments in modal logic. Generally, computers are very adept at processing sentences with truth-functional operators, but non-truth-functional operators are more complicated. Since a goal in the field of Artificial Intelligence is to allow computers to reason as humans do, making them capable of reasoning about possibilities (not just probabilities) seemed helpful. I started with S5, since it seemed like one of the most well-known systems of modal logic.