기계가 문제를 확인할 수 있도록 중단 문제에 대한 Turing의 증거를 공식화하고 싶다고 가정합니다. 잘 알려진 자동 정리 증명 시스템 중 일부는 Mizar, Coq 및 HOL4를 포함합니다. Coq을 다운로드하여 실험했지만 Turing 머신을위한 라이브러리가 없습니다. 나는 스스로 코드를 작성하려고 생각했지만 튜토리얼이 부족하고 언어를 선택하기가 어렵다는 것을 알았습니다.
내 질문은 : 일반적으로 튜링 기계와 관련된 이론을 증명하는 데 유용한 자동 정리 증명자가 있습니까? 나는 이미 존재하는 라이브러리를 사용하여 정지 문제의 결정 불가능 성을 증명할 수 있다면 그러한 정리 증명 자 “좋은”것을 고려할 것입니다. 상대적으로 픽업하기가 쉽다면 더 좋을 것이라고 생각합니다. (기록을 위해, 나는 보통 프로그래밍 언어에 어려움이 없습니다.)
감사,
필립
답변
다음은 라이스 정리가 포함 된 Isabelle / HOL 라이브러리로, 광범위한 문제의 결정 불가능 성을 나타냅니다. 이 라이브러리는 재귀 함수를 통해 계산 기능을 모델링하기 때문에 튜링 기계의 정지 문제를 결정할 수 없는지 증명하기 위해이 정리를 사용하려면 범용 Turing 기계를 재귀 함수로 인코딩해야합니다. 그러나 결정 불가능한 증거의 필수 부분은 이미 완료되었습니다.
http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html