Apakah ada tempat penyimpanan untuk hierarki bukti?

15

Saya adalah asisten bukti belajar mandiri dan memutuskan untuk memulai pada beberapa bukti dasar dan terus maju. Karena bukti didasarkan pada bukti lain dan karenanya membentuk hierarki, adakah repositori dari hierarki bukti?

Saya tahu saya dapat memilih asisten bukti dan menganalisis perpustakaannya untuk mengekstrak hierarki, namun jika saya ingin menemukan bukti berikutnya dalam sebuah rantai untuk membuktikan, saya tidak bisa ketika itu tidak ada di perpustakaan.

Dalam pikiran saya, saya menggambar grafik, mungkin DAG , dari semua bukti matematika yang diketahui yang dapat diekspresikan menggunakan pernyataan bahasa Inggris, bukan bukti menggunakan gambar . Ini akan menjadi peta master (peta dalam arti mulai dari satu titik dan bepergian ke titik lain melalui titik-titik perantara), dan untuk asisten bukti tertentu, seseorang akan memiliki subgraf dari peta master. Kemudian jika seseorang ingin membuat bukti menggunakan asisten bukti yang ditemukan pada master bukan pada subgraph, dengan membandingkan dua grafik seseorang bisa mendapatkan ide tentang pekerjaan yang diperlukan untuk membuat bukti yang hilang (s) untuk asisten bukti.

Saya sadar bahwa bukti matematis tidak selalu mudah dikonversi untuk digunakan dengan asisten bukti, namun memiliki gagasan umum tentang apa yang harus dilakukan jauh lebih baik daripada tidak sama sekali.

Juga dengan memiliki peta master, saya dapat melihat apakah ada jalur mulitple dari satu titik ke antoher dan memilih jalur yang lebih dapat diterima untuk asisten bukti partikular.

EDIT

Dalam pencarian saya menemukan sesuatu yang mirip dengan fungsi matematika . Saya tidak menemukan satu untuk bukti di NIST

reference-request logic proof-assistants Guy Coder
sumber
1
Apakah Anda mencari repositori kode (untuk sistem bukti tersebut), atau "repositori" bukti umum (ditulis dalam Bahasa Inggris / notasi matematika)? Jika yang terakhir, pernahkah
Nicholas Mancuso
Saya akan terkejut menemukan repositori bukti yang terstruktur dan komprehensif. Selain itu, setiap buku matematika adalah satu.
Raphael
1
@NicholasMancuso Tampak menjanjikan. Klausa "dari" dalam definisi bukti muncul untuk memberikan apa yang saya butuhkan. Saya tahu daftar ini tidak besar ~ 5.000 tetapi sebagai pemula mungkin cukup peta bagi saya untuk memulai. Buat jawaban dan saya akan memberikan Anda suara.
Guy Coder
1
Saya tidak yakin grafik seperti itu ada - ada pernyataan dalam matematika yang tidak selalu mengikuti langsung dari serangkaian bukti lainnya. Banyak argumen geometris termasuk dalam kategori ini. Dimungkinkan untuk mengisinya, tetapi mungkin ada poin di mana tidak ada yang mau repot-repot membuktikan "jelas". Jika grafik seperti itu ada, saya pikir itu akan benar-benar besar, baik dalam ukuran maupun kedalaman. Saya tidak bisa membayangkan jumlah langkah untuk mendapatkan dari ZFC ke rumus kuadratik, apalagi Teorema Terakhir Fermat.
SamM

Jawaban:

11

Sistem Mizar adalah gudang besar bukti matematika. Lihat halaman wikipedia dan situs web resmi .

dari semua bukti matematika yang diketahui yang dapat diekspresikan menggunakan pernyataan bahasa Inggris

Dari wikipedia / Mizar_system # Mizar_language :

Fitur khas dari bahasa Mizar adalah keterbacaannya

Bukti ditulis sebagai artikel, yang mana ada lebih dari seribu artikel, dan lebih dari 50.000 teorema yang terbukti. Halaman wikipedia menyebutkan beberapa ide menarik dari " manifesto QED ", dan bagaimana Mizar mungkin dalam perjalanan untuk mencapai ini.

Realz Slaw
sumber
Saya tahu perpustakaan Mizar tetapi tidak tahu tentang grafik. Saya menantang untuk melihat ini ketika saya mendapat kesempatan.
Guy Coder
9

ProofWiki berisi sejumlah bukti yang layak dari berbagai bidang matematika. Ini tidak berarti lengkap, tetapi merupakan titik awal yang baik untuk apa yang Anda inginkan.

Nicholas Mancuso
sumber
8

Metamath memiliki banyak pilihan bukti, dibangun langsung dari inti mereka dalam logika proposisional.

Yang mengatakan, itu sangat kurang dalam hal teori CS. Jangan ragu untuk mengembangkannya!

Ya ampun
sumber
Saya melihat sekilas, ini terlihat menjanjikan.
Guy Coder
4

Lihat arsip TPTP , Ribuan Masalah untuk Teorema Prover. Ini agak standar di lapangan. Ini lebih merupakan "simpul" dari grafik teorema yang Anda tanyakan. Beberapa makalah yang merujuk pada arsip mungkin telah menjelajahi tepi dalam grafik ini.

Perhatikan bahwa di bidang ATM, pembuktian teorema otomatis dan pembuktian teorema bantuan, buktinya simbolis dan tidak benar-benar layak atau masuk akal untuk mempelajari "bukti dalam bahasa Inggris" seperti yang Anda bayangkan.

Namun Anda mungkin belajar tentang paradoks Richard yang dimulai sebagai formulasi bahasa dan kemudian diformalkan secara simbolis. Dikatakan sebagai inspirasi untuk "antimonies" (kontradiksi) yang ditemukan dalam teori himpunan awal yang secara historis bahkan membuka jalan ke teorema ketidaklengkapan Gödel.

vzn
sumber