*To*: Wang Zirui <zirui at nus.edu.sg>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sun, 4 Oct 2009 09:58:31 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <fb295f280910030331l481d704fla52b8e0af1ac5da2@mail.gmail.com>*References*: <fb295f280910030331l481d704fla52b8e0af1ac5da2@mail.gmail.com>

Larry Paulson On 3 Oct 2009, at 11:31, Wang Zirui wrote:

The problem with this is that it's harder to do proofs in a strong theory. Therefore I want to define Turing machine in a weaker theory (with fewer axioms). Basically it would good to have the theory as weak as possible (because it facilitates proofs).

**Follow-Ups**:**Re: [isabelle] Formalizing Turing machine***From:*Wang Zirui

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

- Previous by Date: [isabelle] Haskell code generator problem, upper-case type variables
- Next by Date: Re: [isabelle] Formalizing Turing machine
- Previous by Thread: Re: [isabelle] Formalizing Turing machine
- Next by Thread: Re: [isabelle] Formalizing Turing machine
- 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