Email Gateway (Aug 22 2022 at 15:17): Email Gateway (Aug 22 2022 at 15:17):From: Ken Kubota <mail@kenkubota.de>
Dear List Members,
An earlier statement of mine in the HOL and Isabelle mailing lists on R0 has
to be corrected. The claim that "Unlike all other existing proof assistants or
proof checkers, it is a Hilbert-style system", has to be relativized, since,
depending on how strictly a Hilbert-style system is defined, Metamath may be
considered a Hilbert-style system, too:
"Natural Deduction in the Metamath Proof Explorer (MPE)
MPE is fundamentally a Hilbert-style system."
http://us.metamath.org/mpegif/mmnatded.html
Another discovery is Cris Perdue's implementation of a natural deduction
variant of Peter B. Andrews' logic Q0 at
prooftoys.org
and
mathtoys.org
Although the equation solver is quite strong and impressive, Cris Perdue
considers his implementation as "work in progress". Interestingly, it seems as
if independently in same cases for this variant of Q0 exactly the same design
decisions were made as for R0, in particular, the replacement of the turnstile
by the logical implication, and the corresponding implementation of Rule R'.
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10.4444/100
Last updated: Nov 21 2024 at 12:39 UTC