Jedną z rzeczy, które moim zdaniem będą interesujące, jest to, że termin „dowodzenie twierdzenia” różni się znacznie w zależności od dziedziny, w której się znajdujesz. Chociaż są one - w sposób abstrakcyjny - nieco powiązane, praktyczne dowodzenie twierdzeń (takie jak patrz rozwinięte w Handbook of Automated Reasoning) ma mniej wspólnego z Coq lub Isabelle, niż mogłoby się wydawać.
Kiedy po raz pierwszy zacząłem uczyć się o twierdzeniu dowodzącym pokrewnych rzeczy, pierwszą książką, którą przeczytałem (chociaż teraz dość przestarzałą?) Była doskonała logika pierwszego rzędu i automatyczne dowodzenie twierdzeń Melvina Fittinga. Ta książka była naprawdę doskonała i obejmowała rodzaje tematów, które zobaczysz, które dotyczą logiki niższego rzędu, w której można uzyskać całkiem sporo automatyzacji. Logika, której się uczysz, powinna być podyktowana tym, o czym chcesz wnioskować, a nie tyle twierdzeniem, które z tego powodu. Na przykład, podczas gdy logika pierwszego rzędu zapewnia dużą ekspresję i umiejętność rozumowania, większość społeczności języków programowania (w której ostatnio skończyłem) opuściła starszą szkołę dowodzenia twierdzeń i sprawdzania modeli (które wchodzą w koszyk rzeczy, które są bardziej rozstrzygalne, ale mniej wyraziste).
Nie oznacza to jednak, że takie rzeczy, jak wnioskowanie pierwszego rzędu i sprawdzanie modelu, nie były wyjątkowo przydatne w praktyce. Oni byli! Możesz spojrzeć na ACL2 jako przykład provera zbudowanego na logice pierwszego rzędu, który ma niesamowity sukces w sferze przemysłowej. Oprócz tego nastąpił niesamowity rozwój rozwiązań w zakresie SMT. Nowoczesne solwery SMT są zbudowane na bardzo potężnych solverach SAT (głównie dzięki odkryciom w ciągu ostatnich dwudziestu lat w celu ulepszenia DPLL) i znalazły wiele zastosowań w symbolicznych wykonaniach.
Jednak, jak już powiedziałem, chociaż bardziej tradycyjny „dowodzenie twierdzenia” jest zabawny, jest o wiele więcej do nauczenia się. Nauka uczenia się - na przykład - ma niewiele wspólnego z uczeniem się narzędzi automatyzacji, które ci daje, i ma znacznie więcej wspólnego z uczeniem się teorii typów, na której się opiera (rachunek predykcyjny konstrukcji koindukcyjnych). Jeśli nie jesteś przyzwyczajony do konstruktywnej logiki, izomorfizmu curry Howarda lub teorii typów, będziesz miał ekscytujący czas na naukę tych narzędzi, ale trudno mi pomyśleć, że są zbyt blisko związane z rzeczami, które zobaczysz w pierwszym tomie podręcznika.
Zdecyduj więc, co chcesz zrobić: zweryfikuj modele i twierdzenia w logice pierwszego rzędu lub użyj potężnej teorii typów, aby uzasadnić poprawność swoich programów (lub twierdzeń w logice konstruktywnej). Jeśli to pierwszy, dowiedz się więcej o technikach opartych na zautomatyzowanej dedukcji, jeśli to drugi, dowiedz się więcej o Coq, HOL itp. Nawiasem mówiąc, jeśli chcesz nauczyć się Coq, a powyższe odniesienia są dobre, myślę, że istnieją dwa podstawowe odniesienia do nauki języka Coq:
Książka założycieli Benjamina Pierce'a (Dr. Pierce jest znakomitym pisarzem. Polecam również przyjrzeć się jego bardziej popularnej „książce z cegły”, jeśli jeszcze tego nie zrobiłeś).
Certyfikowane programowanie z typami zależnymi (Adam Chlipala również pisze całkiem dobrze, chociaż jego książki zakładają nieco więcej dojrzałości i inteligencji niż być może prostsze wprowadzenie Pierce'a).