Stream: Beginner Questions

Topic: Why natural deduction?

view this post on Zulip waynee95 (May 02 2022 at 17:13):

Why does Isabelle (and most other proof assistants) use natural deduction as opposed to sequent calculus?

I don't remember which paper exactly but in one paper by (I think) Lawrence Paulson he said something along those lines of "Isabelle originally used sequent calculus but I switched to natural deduction because deriving rules is easier".

Last updated: Feb 27 2024 at 08:17 UTC