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.
On 3 Oct 2009, at 11:31, Wang Zirui wrote:
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