5

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.

Improve this question

1 Answer 1

Reset to default
1

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 purposes, by Christoph Benzmuller et al. - you can find links to their work here: http://page.mi.fu-berlin.de/cbenzmueller/compmeta/htdocs/

Improve this answer
0

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .