Kategorisasi dalam daftar itu tentu saja masih terkini.
Mungkin satu kategori baru telah muncul, yaitu, bahasa pemrograman bertipe dependen . Ini pada dasarnya pembuktian teorema otomatis di mana tujuan utama bukan pembuktian teorema, melainkan pemrograman. Karena korespondensi Curry-Howard , kedua konsep ini sangat terkait. Tujuan akhir dari bahasa pemrograman tersebut adalah untuk menulis program yang memiliki jaminan lebih kuat daripada bahasa pemrograman yang diketik biasa. Orang-orang juga menggunakan ini untuk membuktikan teorema. Beberapa sistem baru termasuk dalam kategori ini termasuk Agda dan Epigram. Salah satu karakteristik utama dari bahasa-bahasa tersebut adalah bahwa mereka berupaya keras agar programmer lebih mudah mendefinisikan keluarga tipe data induktif. Contoh sederhana adalah vektor, yang tergantung pada bilangan asli (didefinisikan secara induktif).
Mengenai yang masih sangat aktif, saya pikir semuanya. Coq , Isabelle , Twelf , dan PVS banyak digunakan dalam komunitas bahasa pemrograman. Maude digunakan secara luas dalam sistem pemodelan. (Secara pribadi, saya telah menggunakan Coq dan Maude .)
Saya belum pernah mendengar tentang beberapa dari mereka. Dalam pdf yang Anda tautkan, ada tautan ke pembalik teorema. Beberapa tautan terkini, beberapa rusak. Gandalf sekarang tampaknya semacam penyihir berjanggut.
Provers teorema yang disebutkan dalam “A Review of Theorem Provers” adalah:
- ALF : dibuat oleh ALFA, Coq, dan Agda.
- ALFA : tampaknya tidak lagi tidak didukung.
- COQ : didukung secara aktif.
- MetaPRL : tampaknya tidak lagi didukung.
- NuPRL : didukung secara aktif.
- HOL : didukung secara aktif.
- PVS : didukung secara aktif.
- Isabelle : didukung secara aktif.
- DUA BELAS : didukung secara aktif.
- ACL2 : didukung secara aktif.
- INKA : sepertinya tidak lagi didukung.
- GANDALF : tampaknya tidak lagi didukung.
- TPS : mungkin masih aktif, tetapi hanya memiliki sedikit pengikut.
- OTTER : mungkin tidak lagi didukung.
- SETHEO : diganti oleh E-SETHEO, yang tampaknya tidak lagi didukung.
- SPASS : sepertinya masih aktif.
- EQP : tampaknya tidak lagi didukung.
- MAUDE : sangat aktif didukung.
- OMEGA : tampaknya tidak lagi didukung.
- Mizar : didukung secara aktif.
Tidak diragukan lagi banyak teorema teorema otomatis baru yang belum disebutkan dalam daftar ini.
Untuk kelengkapan, seperti yang disarankan oleh Raphael , ada bukti pengarsipan situs yang dibuat menggunakan berbagai alat. Sebagai contoh:
