[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: 


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.