Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it.  Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4.  I downloaded and experimented with Coq, but it doesn't have a library for Turing machines.  I thought to code one myself, but found the tutorial lacking and the language difficult to pick up.My question is:  Is there an automated theorem prover that is generally good at proving theorems that involve Turing machines?  I would consider such a theorem prover good if it can formalize a proof of the undecidability of the halting problem using already-existing libraries.  I would consider it even better if it's relatively easy to pick up.  (For the record, I don't usually have difficulty with programming languages.)Thanks,Philip
Is there a reasonable automated proof system for TCS theorems?
lo.logic;turing machines;software;proof assistants;automated theorem proving
Here is an Isabelle/HOL library containing Rice's theorem, which states undecidability of a wide range of problems. Since this library models computability via recursive functions, you have to encode a universal Turing machine as a recursive function in order to use this theorem for proving undecidability of the halting problem of Turing machines.  However, the essential parts of the undecidability proof is already done.http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html