Is there a reasonable automated proof system for TCS theorems?

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

Asked by user186 (5,070 )
Jan 14, 2011 at 00:32