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.

He provides instructions on how to use it on the main page and examples (and explanations) here. Check it out!

I’d be curious to know whether others have used this sort of thing in teaching, and how. This tool looks really cool, so I’d love to make use of it.

For anyone interested in this kind of thing: I recently released a program that can check if a first order sentence is satisfied by a model (among many other things). It is freely available at my personal website: Your email address will not be published. Read more from…

thumbnail courtesy of