*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Wang Zirui <zirui at nus.edu.sg>*Date*: Sun, 4 Oct 2009 17:44:49 +0800*In-reply-to*: <D8FA391C-418C-48CB-8CA6-FF7798F6D2C3@cam.ac.uk>*References*: <fb295f280910030331l481d704fla52b8e0af1ac5da2@mail.gmail.com> <D8FA391C-418C-48CB-8CA6-FF7798F6D2C3@cam.ac.uk>

OK, maybe it's a bad choice to start with formalizing Turing machine, which is a definition not a theorem. How about formalizing Cook's theorem, the Probabilistically Checkable Proof (PCP) theorem and the natural proof theorem? Yes, I'm very interested in formalizing theorems in computational complexity theory. Has anyone done this? Zirui Wang

**References**:**Re: [isabelle] Formalizing Turing machine***From:*Wang Zirui

**Re: [isabelle] Formalizing Turing machine***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Formalizing Turing machine
- Next by Date: Re: [isabelle] Haskell code generator problem, upper-case type variables
- Previous by Thread: Re: [isabelle] Formalizing Turing machine
- Next by Thread: Re: [isabelle] Discrete Summation
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list