[isabelle] finally published online: GÃdelâs Incompleteness Theorems



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.