Solvers for modal epistemic logics

Question

Is there any (SMT-like) solvers for modal epistemic logics (aka logic of knowledge)?

I need First Order (not just propositional) case.

Answer 1

Here are some relevant links:

Modal logic solvers:

• http://www.cs.man.ac.uk/~schmidt/tools/
• http://www.irit.fr/Lotrec/
• http://twan.home.fmf.nl/moltap/index.html
• http://www2.tcs.ifi.lmu.de/~mlange/papers/m4m-6.pdf

Description logic reasoners:

• http://www.cs.man.ac.uk/~sattler/reasoners.html

Dynamic Epistemic Modelling, mentioned in Pal's answer.

• http://homepages.cwi.nl/~jve/demo/DEMO.pdf

Unfortunately all of them (AFAIK) work only in propositional (not first order) case.

Answer 2

You can try the model checker DEMO (Dynamic Epistemic MOdelling).