Rodzaje automatycznych dostawców twierdzeń

^{Uczę się samodzielnie Automated Theorem Proving / SMT solvers / Proof Assistants i piszę serię pytań na temat tego procesu, zaczynając tutaj .}

Jakie są odpowiednie dowody zautomatyzowanego twierdzenia? Znalazłem Przegląd dostawców twierdzeń

Czy to wciąż aktualne?

Które są nadal bardzo aktywne, tj. Które są obecnie używane poza grupą, która je utworzyła?

^{Znajdź następne pytanie z serii tutaj .}

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:

• Archiwum oficjalnych dowodów dla Isabelle
• Sformalizowana matematyka dla Mizara
• Konstruktywne repozytorium Coq
• Katalog książek ACL2
• Wybory z biblioteki matematycznej PRL
• Biblioteki PVS NASA Langley