Re: [isabelle] Formalizing Turing machine

You are quite right to be concerned about difficulty of proofs, but there are many factors involved in this difficulty, and some weak theories are much more difficult to use than stronger theories. If you want to accomplish your project with the minimum of effort, you should undoubtedly choose Isabelle/HOL. Not only is the logic easy-to-use; the implementation provides lots of automation.

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).

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