waynee95 (May 02 2022 at 17:13): 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 01 2025 at 20:19 UTC