Apakah ada sistem bukti otomatis yang masuk akal untuk teorema TCS?

28

Misalkan saya ingin memformalkan bukti Turing mengenai masalah penghentian sehingga mesin dapat memeriksanya. Beberapa sistem pembuktian teorema otomatis yang terkenal meliputi Mizar, Coq, dan HOL4. Saya mengunduh dan bereksperimen dengan Coq, tetapi tidak memiliki perpustakaan untuk mesin Turing. Saya berpikir untuk membuat kode sendiri, tetapi menemukan tutorialnya kurang dan bahasa sulit untuk diambil.

Pertanyaan saya adalah: Apakah ada pembuktian teorema otomatis yang umumnya bagus dalam membuktikan teorema yang melibatkan mesin Turing? Saya akan menganggap teorema seperti itu "bagus" jika itu dapat memformalkan bukti ketidaktentuan masalah berhenti menggunakan perpustakaan yang sudah ada. Saya akan mempertimbangkannya lebih baik jika relatif mudah diambil. (Sebagai catatan, saya biasanya tidak mengalami kesulitan dengan bahasa pemrograman.)

Terima kasih,

Philip

lo.logic turing-machines software proof-assistants automated-theorem-proving Philip White
sumber
Anda mungkin ingin memeriksa halaman ini tetapi daftar tidak termasuk masalah penghentian.
Kaveh
10
Saya berani mengatakan bahwa Anda perlu bertahan dengan sesuatu seperti Coq sebelum akan terasa alami. Dan Anda harus berada di terminal untuk menyelesaikan masalah, daripada membaca buku. Mendapatkan "Pembuktian Teorema Interaktif dan Pengembangan Program: Coq'Art: The Calculus of Inductive Constructions" akan membantu. Tutorial Coq: cis.upenn.edu/~bcpierce/sf dan adam.chlipala.net/cpdt cukup bagus (meskipun tidak ditujukan langsung pada apa yang Anda inginkan).
Dave Clarke
5
Formalisasi sebuah bukti bisa sangat rumit jika Anda memilih versi yang "salah". Untuk masalah Berhenti, saya sarankan untuk membuktikan versi yang lebih umum dan abstrak terlebih dahulu. Maka Anda dapat membuktikan nanti bahwa mesin Turing adalah kasus khusus dari versi abstrak, jika Anda masih ingin melakukannya (akan ada banyak detail yang membosankan tentang mesin Turing jadi mungkin waktu akan lebih baik dihabiskan dengan melakukan hal lain). Saya akan memikirkan cara yang baik untuk membuktikan ini dalam Coq. Tetap disini.
Andrej Bauer
5
Jika Anda pandai matematika dan pandai pemrograman, maka Anda memiliki prasyarat untuk belajar bagaimana menggunakan asisten bukti. Anda benar-benar perlu memperlakukannya sebagai keterampilan baru. (Namun, ini sangat bermanfaat.)
Neel Krishnaswami
Sepertinya jawaban untuk pertanyaannya adalah "tidak". Sistem seperti itu akan sangat berguna menurut saya - bolehkah saya meminta jika Anda memformalkan mesin Turing, dapatkah Anda memberikan sedikit pemikiran untuk kesetaraan waktu polinomial?
Colin McQuillan

Jawaban:

17

Berikut ini adalah perpustakaan Isabelle / HOL yang berisi teorema Rice, yang menyatakan ketidakpastian berbagai masalah. Karena perpustakaan ini memodelkan komputabilitas melalui fungsi rekursif, Anda harus menyandikan mesin Turing universal sebagai fungsi rekursif untuk menggunakan teorema ini untuk membuktikan keraguan tentang masalah penghentian mesin Turing. Namun, bagian-bagian penting dari bukti yang belum dipastikan sudah dilakukan.

http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html

yhirai
sumber