I am looking for a proof checker for modal logic using natural deduction or sequent calculus.

I am trying to learn Isabelle, but I think there should be a simpler solution.

Although I can rely on mentally checking proofs I realize it is very easy to make mistakes and I do not trust my ability to manually check even simple proofs.

I will list here some possibilities I am exploring:

  1. Ross Kirsling's Modal Logic Playground

  2. Another useful resource is Frederic Fitch's Symbolic Logic: An Introduction. He lists the natural deduction rules for various modal logics. David F. Siemens, Jr, "Fitch-Style Rules for Many Modal Logics" Notre Dame Journal of Formal Logic Volume XVIII, Number 4, October 1977 summarize these. These are not proof checkers, but provide what one should expect to see in a proof checker.

  3. @DanChristensen has a proof checker, DC Proof, that allowed him to derive the axioms for modal logic from first order logic using the standard translation.


Another possibility is MleanCoP: http://www.leancop.de/mleancop/

I also think Isabelle is worth the effort. It's been adapted to modal logic, for philosophical purposed, by Christoph Benzmuller et al. - you can find links to their work here: http://page.mi.fu-berlin.de/cbenzmueller/compmeta/htdocs/

  • Thank you, I will try both of them. – Frank Hubeny Dec 12 '18 at 13:56

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.