An Automated Modal Reasoner

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!

David Roy, “Labyrinth”

There are 11 comments

Your email address will not be published. Required fields are marked *

Please enter an e-mail address