Kategoryzacja na tej liście jest z pewnością wciąż aktualna.
Być może pojawiła się jedna nowa kategoria, a mianowicie języki programowania o typie zależnym . Są to zasadniczo zautomatyzowane dowody twierdzeń, w których głównym celem nie jest dowodzenie twierdzeń, ale programowanie. Ze względu na korespondencję Curry-Howarda te dwa pojęcia są ze sobą ściśle powiązane. Ostatecznym celem takich języków programowania jest pisanie programów, które mają znacznie silniejsze gwarancje niż zwykłe języki programowania. Ludzie używają ich również do dowodzenia twierdzeń. Niektóre nowe systemy należące do tej kategorii to Agda i Epigram. Jedną z kluczowych cech takich języków jest to, że wkładają wiele wysiłku w ułatwienie programistom definiowania indukcyjnych rodzin typów danych. Prostym przykładem jest wektor, który zależy od liczb naturalnych (zdefiniowanych indukcyjnie).
Jeśli chodzi o to, które z nich są nadal bardzo aktywne, myślę, że wszystkie są. Coq , Isabelle , Twelf i PVS są często używane w społeczności języków programowania. Maude jest szeroko stosowany w systemach modelowania. (Osobiście korzystałem z Coq i Maude .)
Nigdy nie słyszałem o kilku z nich. W pliku pdf, do którego prowadzi link, znajdują się linki do dowodów twierdzeń. Niektóre linki są aktualne, niektóre są zepsute. Gandalf wygląda teraz na jakiegoś brodatego czarodzieja.
Dowody twierdzeń wspomniane w „Przeglądzie dostawców twierdzeń” to:
- ALF : objęty przez ALFA, Coq i Agda.
- ALFA : wydaje się już nieobsługiwany.
- COQ : aktywnie wspierany.
- MetaPRL : wydaje się nie być już obsługiwany.
- NuPRL : aktywnie wspierany.
- HOL : aktywnie wspierany.
- PVS : aktywnie wspierany.
- Isabelle : aktywnie wspierana.
- TWELF : aktywnie wspierany.
- ACL2 : aktywnie wspierany.
- INKA : wydaje się, że nie jest już obsługiwany.
- GANDALF : wydaje się nie być już obsługiwany.
- TPS : może być nadal aktywny, ale ma tylko niewielką liczbę osób.
- OTTER : może już nie być obsługiwany.
- SETHEO : zastąpiony przez E-SETHEO, który wydaje się nie być już obsługiwany.
- SPASS : wydaje się być nadal aktywny.
- EQP : wydaje się, że nie jest już obsługiwany.
- MAUDE : bardzo aktywnie wspierany.
- OMEGA : wydaje się, że nie jest już obsługiwany.
- Mizar : aktywnie wspierany.
Niewątpliwie istnieje wiele nowych automatycznych dowodów twierdzeń, które nie zostały wymienione na tej liście.
Dla kompletności, jak sugeruje Raphael , istnieją dowody archiwizacji stron wykonane przy użyciu różnych narzędzi. Na przykład:
