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: Dec 21 2024 at 16:20 UTC