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”
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: https://sites.google.com/view/ariel-roffe/software
You probably didn’t mean this, but it’s very natural to read your comment as claiming that you have a program that can check whether a first-order sentence has a model (which is impossible).
(You can take that as an invitation to explain just exactly what your program can do. I wasn’t able to find out because I’m a Mac user and it only runs on Windows.)
Haven’t checked, but I presumed it meant: given a sentence S and interpretation M for the language of S, the program can check if S is true or false in M. That doesn’t violate metalogic and is still plainly useful!
C
(Can’t work in full generality, though. Otherwise: ask it whether the Goldbach conjecture holds in the standard model of arithmetic plz! was thinking of finite models, for checking simple homework exercises.)
Yes. I was about to say that if it could do that then arithmetic would be not only complete but decidable
Exactly. You specify a language L, an interpretation of the language M and a sentence S, and the program tells you if S is true or false (or indeterminate*) in M.
Interpretations can be infinite (e.g. you can refer to the natural numbers and the real numbers), but all quantifiers must be bounded to finite sets. That is how the problem becomes decidable.
* Interpretations can have denotation failures (terms for which the denotation is not specified). The program uses a non-classical logic to treat them. Otherwise it behaves classically.
Here is a collection of links to similar tools, and for dynamic epistemic logic, temporal logic, PDL, and others: http://www.cs.man.ac.uk/~schmidt/tools/
Also: use the program linked in this post at your own risk, as it has some substantial bugs. For instance, it reports N(p>q)>(Np>Nq) to be invalid, among other mistakes.
The bugs found by readers entering the following inputs have been fixed now:
a) N(p>q)>(Np>Nq)
b) (p&(p>q))>q
I haven’t formally proven the correctness of the program, so, yes, use at your own risk. I will continue to add test cases, to reduce the chance of a user encountering one. Let me know if you come across any other bugs. Thanks.