Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] finally published online: Gödel’s Incompletene...

view this post on Zulip Email Gateway (Aug 22 2022 at 09:35):

From: Larry Paulson <lp15@cam.ac.uk>
A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle

“… The Isabelle formalisation uses two separate treatments of variable binding: the nominal package… and de Bruijn indices … . Critical details of the Isabelle proof are described, in particular gaps and errors found in the literature."

Now available online at SpringerLink:

http://link.springer.com/article/10.1007/s10817-015-9322-8

Paywalled, but full texts available here: http://www.cl.cam.ac.uk/~lp15/papers/Formath/

Larry Paulson

Last updated: Nov 21 2024 at 12:39 UTC