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”

guest
11 Comments
Oldest
Newest Most Voted
Inline Feedbacks
View all comments
P
P
2 years ago

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.Report

Ariel Roffé
2 years ago

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/softwareReport

Juhani Yli-Vakkuri
Reply to  Ariel Roffé
2 years ago

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).Report

Juhani Yli-Vakkuri
Reply to  Juhani Yli-Vakkuri
2 years ago

(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.)Report

Chris Scambler
Chris Scambler
Reply to  Juhani Yli-Vakkuri
2 years ago

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!

CReport

Chris Scambler
Chris Scambler
Reply to  Chris Scambler
2 years ago

(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.)Report

Juhani Yli-Vakkuri
Reply to  Chris Scambler
2 years ago

Yes. I was about to say that if it could do that then arithmetic would be not only complete but decidableReport

Ariel Roffé
Ariel Roffé
Reply to  Chris Scambler
2 years ago

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.Report

Josh Fry
Josh Fry
2 years ago

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/

Report

Josh Fry
Josh Fry
2 years ago

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.Report

Brian Tackett
Reply to  Josh Fry
2 years ago

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.Report