Isabelle supports many different logics, and it has a formulation of first order logic which you may browse here: http://isabelle.in.tum.de/dist/library/FOL/index.html. However, even though proofs are natural deduction in flavor, it does not produce anything a logician would understand as a natural deduction derivation upon shallow inspection.
The automated theorem provers Prover9, E, SPASS and Vampire are all first order systems. They do not produce proofs using natural deduction (they are all typically resolution/paramodulation based systems).
It sounds like ProofWeb is exactly like what you want. It provides a system for displaying the accompanying natural deduction/sequent calculus proof along with a computer assisted formalization. It also has a really nice interactive interface for students, and provides the possibility of assigning exercises. On the other hand, I know that it has been largely developed for Coq, which is way, way more expressive than first order logic. And even though I know that there is a development of set theory within Coq, I suspect modifying the system for basic set theory would be a nontrivial exercise.
No comments:
Post a Comment