- lo.logic turing-machines software proof-assistants automated-theorem-proving
- Updated Sun, 29 May 2022 17:29:17 GMT

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

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

External links referenced by this document: