Po przeczytaniu twojego pytania jedynym sposobem, w jaki mogłem zobaczyć i mieć wystarczającą wiedzę, aby powiązać ze sobą tematy, było przekazanie zestawu artykułów na wysokim poziomie, które przechodzą od weryfikacji oprogramowania, kończąc na próbie połączenia sprawdzania modelu i dowodzenia twierdzeń. Mam nadzieję, że mój komentarz to zrobił:
Spójrz na weryfikację oprogramowania, następnie weryfikację formalną, a następnie kontrolę modelu i formalną weryfikację oprogramowania: kontrola modelu i sprawdzanie twierdzeń
Dave udzielił dobrej odpowiedzi, na którą nie mogę zrobić więcej sprawiedliwości w pierwszej części pytania niż Dave, ponieważ jestem w tym również nowy.
Ponieważ jest to twoje pierwsze pytanie na stronie SE , powodem, dla którego nie dałem odpowiedzi, ale komentarz, jest to, że tutaj odpowiedź nie może być tylko zbiorem linków, ale musi dać pisemną odpowiedź i użyć linków na poparcie odpowiedzi; stąd komentarz zamiast odpowiedzi.
Z pozdrowieniami dla:
Wszelkie wskazówki do książek lub artykułów dla początkujących w tej sprawie są bardzo mile widziane.
Książki, które polecam i których używam to:
Logika w informatyce - modelowanie i rozumowanie dotyczące systemów 2nd Ed. autor: Huth i Ryan Wprowadza to logikę i przechodzi do sprawdzania modelu, ale nie przechodzi do dowodzenia twierdzeń. Powinno to obejmować wszystkie podstawowe pytania związane z logiką i sprawdzaniem modelu.
Zasady sprawdzania modeli przez Baiera i Katoena Właśnie zacząłem czytać ten i jest to o wiele lepsze niż czytanie wielu artykułów i próba sprawdzenia, jak wszystkie one do siebie pasują. Jest to jedna z najbardziej, jeśli nie najbardziej zalecana książka na temat sprawdzania modelu. Powinien odpowiedzieć na bardziej zaawansowane pytania dotyczące sprawdzania modelu.
Logika czasowa i systemy stanowe Krogera i Merza Często lubię mieć książki różnych autorów podczas samodzielnego uczenia się przedmiotu. Ten ma uzupełnić / uzupełnić „Zasady sprawdzania modelu”
Podręcznik praktycznej logiki i automatycznego rozumowania Harrison Będąc programistą Nie mogę wystarczająco polecić tej książki. Książka zaczyna się od wprowadzenia logiki i przechodzi przez etap tworzenia jądra dla dowcipnisia opartego na pracy HOL Light . Żeby podkreślić, że książka używa działającego kodu OCaml, wyjaśnia te twierdzenia w kategoriach, które uważam za przyjazne, i daje ci to, co musisz wiedzieć, ale nie tak bardzo, że nie możesz nawiązać połączenia ani poczuć, że biegniesz w dół. If jest bardzo skoncentrowaną książką na temat przejścia od logiki do określonego rodzaju twierdzenia twierdzącego.
Jak to udowodnić: ustrukturyzowane podejście Vellemana Aby dostać się do asystentów Proof dla twierdzenia dowodzącego, że będziesz musiał żyć i spać twierdzenia.
Wprowadzenie do dowodów i języka matematycznego według dnia Jest to bezpłatna książka, która nie tylko uzupełnia „Jak to udowodnić”, ale w sumie wykracza poza nią. Nie zdziwiłbym się, gdy ten stał się popularny.
W chwili obecnej nie mogę rozwinąć więcej o dowodzeniu twierdzeń, ponieważ wciąż uczę się zalet / wad i różnic każdego z nich, ale te, na których się skupiam, to
- HOL Light dzięki książce Johna Harrisona.
- Coq, ponieważ opiera się na rachunku konstrukcji
Isabelle, ponieważ opiera się na unifikacji wyższego rzędu.
Ci asystenci ds. Proofów zazwyczaj mają także książki, są aktualni, popularni, mają otwarte oprogramowanie, utrzymują i mają aktywne społeczności wsparcia.
Uwaga: Użyłem worldcat.org, aby odnieść się do książek, ale możesz je przejrzeć za pomocą funkcji Amazon zajrzyj do środka.