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: Jun 20 2024 at 12:31 UTC