Masalah matematika macam apa yang dapat dipecahkan oleh pembalik teorema otomatis?

Bisakah saya membuktikan pernyataan berikut dengan menggunakan pembuktian teorema otomatis yang tersedia?

. $(a+b)^2=a^2+b^2+2ab$
Jika , maka . $11 \mid 2a-3b$ $11 \mid 7a-5b$
Jika , maka $ax^2+bx+c=0$ . $x=\frac{-b\pm\sqrt{b^2-4ac} }{2a}$
Jika genap maka genap. $a$ $4a$

dan seterusnya!

Saya mengajukan pertanyaan ini karena saya baru saja menemukan aplikasi pembuktian teorema Otomatis dalam membuktikan teorema dalam logika.

automated-theorem-proving Benteng matematika
sumber

Anda tentu dapat membuktikan semua ini (kecuali mungkin 3, yang salah ditulis) menggunakan semua asisten bukti standar, meskipun mungkin tidak otomatis.

Yuval Filmus

@YuvalFilmus. Terima kasih! Jadi masalah apa yang bisa diselesaikan secara otomatis?

Math-fort

Anda dapat menyederhanakan ekspresi secara otomatis, meskipun ini adalah layanan yang disediakan oleh Sistem Aljabar Komputer. Saya tidak berpikir asisten bukti modern dapat secara otomatis membuktikan sesuatu yang substansi, meskipun lebih baik untuk bertanya kepada para ahli.

Yuval Filmus

@YuvalFilmus Saya pikir apa yang Anda katakan sering benar, dalam arti bahwa hanya ketika metode bukti otomatis memberikan hasil yang menarik, kami bersedia menyebutnya sebagai bagian dari CAS ...

Kadal diskrit

"(a + b) ^ 2 == a ^ 2 + b ^ 2 + 2ab" di WolframAlpha

Nat

Jawaban:

Sebagian besar pernyataan Anda adalah aljabar dasar, sehingga ini dapat dibuktikan secara otomatis oleh sistem aljabar komputer (CAS), seperti Maple atau Mathematica.

(Jika Anda tertarik pada matematika di balik CAS, saya dapat merekomendasikan buku ini Modern Computer Aljabar oleh Joachim von zur Gathen dan Jürgen Gerhard, sebuah buku yang indah, dianggap sebagai 'alkitab' di lapangan)

Pembuktian teorema otomatis cenderung sebagian besar kasus melakukan pencarian heuristik pada struktur yang mewakili bukti, jika buktinya bukan salah satu dari beberapa kasus yang ada algoritma yang dapat menyelesaikannya secara meyakinkan. Mengingat bahwa pernyataan ini tidak terlalu rumit, ada kemungkinan bahwa prover otomatis dapat 'menemukan' bukti.

Namun, saya pikir menarik untuk mengatakan sedikit lebih banyak tentang pernyataan yang memiliki algoritma yang bagus:

Pernyataan 3 adalah (kasus yang sangat sederhana) tentang akar (sistem) persamaan polinomial dan dapat diselesaikan dengan menemukan basis Gröbner dengan algoritma Buchberger. Dasar Gröbner dan algoritma Buchberger untuk menemukannya adalah alat yang sangat bagus untuk pembuktian teorema otomatis. Sebagai contoh, kita bahkan dapat secara otomatis membuktikan teorema dasar dalam geometri dengan secara otomatis mengubah masalah menjadi akar persamaan polinomial dengan cara yang cerdas!

Kelas teorema lain yang menarik adalah pernyataan yang dapat diekspresikan dalam aritmatika Presburger bebas-kuantifier (khususnya, aritmatika ini tanpa perkalian, jadi ini tidak berlaku untuk pernyataan Anda), karena ada algoritma untuk menyelesaikan semua pernyataan seperti itu, meskipun algoritma agak lambat.

Kadal diskrit
sumber