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
sumber
Jawaban:
Sistem Mizar adalah gudang besar bukti matematika. Lihat halaman wikipedia dan situs web resmi .
Dari wikipedia / Mizar_system # Mizar_language :
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.
sumber
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.
sumber
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!
sumber
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.
sumber