Jak mógłbym zacząć uczyć się podstawowej teorii asystenta dowodu Coq?

Odpowiedzi:

32

Jednym z nich jest podręcznik referencyjny Coq ( pdf ). Rozdział 4 opisuje podstawową logikę Coq i ostatecznie wszystko na tym opiera się. Nazywa się to rachunkiem (ko) konstrukcji indukcyjnych i wiele artykułów opisuje. Zdobycie książki o Coq'Art Interaktywne sprawdzanie twierdzeń i programowanie zapewnia spokojniejsze, ale nie tanie wprowadzenie do Coq.

Aby dowiedzieć się, jak działają taktyki, spójrz na to wcześniejsze pytanie: Jak działają „taktyki” w asystentach dowodowych?

Aby zbudować wymaganą teorię, musisz poznać teorię typów . Najściślej związany z teorią leżącą u podstaw asystenta dowodu jest prawdopodobnie Intutionistic Teoria typów Per Martina- Löfa (lub książka ) lub książka Programowanie w teorii typu Martin-Löf , która tak naprawdę dotyczy pisania i dowodzenia twierdzeń w teorii typów. Perspektywa języka programowania dla teorii typów można uzyskać z Pierce's Types and Programming Languages . Dowody i typy Girarda i in. , Które również odnoszą się do znaczenia korespondencji Curry-Howarda , są kolejnym doskonałym odniesieniem. W takim razie jesteś prawdopodobnie dobrze przygotowany do czytania Coquanda i HuetaRachunek konstrukcji . Na koniec przejrzyj niektóre referencje z tyłu podręcznika Coq.

Są inni asystenci dowodowi , HOL, NuPRL, Mizar, Twelf itd., I mają też swoją teorię, więc możesz się wiele nauczyć, czytając w tym kierunku.

Na koniec, aby zapoznać się z historią i przyszłością asystentów ds. Dowodów, zapoznaj się z najnowszym artykułem Hermana Geuversa.

Dave Clarke
źródło
5
Ładna lista. Dodam kolejność czytania. TAPL Pierce'a obejmuje tło; większość reszty nie ma sensu, dopóki nie opanujesz zasad pisania na klawiaturze. Rozdział 2 ATTAPL stosunkowo delikatnie wprowadza typy zależne. Następnie możesz przeczytać rozdział 4 podręcznika Coq, który zawiera zasady pisania na klawiaturze (musisz sprawdzić bibliografię pod kątem niektórych zaawansowanych rzeczy, takich jak dokładne zasady rekurencji). Równolegle książka Coq'Art ma bardziej praktyczne perspektywy. Dodatkowa wskazówka: Show Treew coq.
Gilles 'SO - przestań być zły'
2
Jestem kimś mniej więcej w tej samej pozycji co OP, choć trochę dalej. Po kilku eksperymentach w końcu znalazłem kolejność 1) Naucz się programowania funkcjonalnego 2) Przeczytaj TAPL 3) Przeczytaj o typach zależnych w ATTAPL, aby działały lepiej niż inne rzeczy. Cieszę się, że jestem na właściwej ścieżce.
John Salvatier,
1
Ja też tu byłem i kupiłem książkę Coq'Art. Jest absolutnie idealny do zrozumienia, szczegółowo omawiają każdą taktykę i wyjaśniają, kiedy i jak z niej korzystać. Książka prowadzi także szybko przez wszystkie podstawowe zasady teorii typów, ucząc notacji i jak używać jej w Coq. Kocham tę książkę.
Lance Pollard,
15

Jeśli chodzi o typowy rachunek lambda, logikę intuicyjną, różne systemy dowodowe i izomorfizm Curry'ego-Howarda, które są częściami matematyki Coq, zdecydowanie polecam „Wykłady na temat izomorfizmu Curry-Howarda” (autor: P. Urzyczyn i M. Sørensen).

Marcin Kotowski
źródło
Wydaje się, że jesteśmy dzisiaj na tej samej długości fali . ;-)
Marc Hamann
Wydaje się być Curry-Howard dzień: cstheory.stackexchange.com/questions/5848/...
Dave Clarke
6

Książka Luo o rozszerzonym rachunku konstrukcji jest również dobrym odniesieniem. ECC wywarło duży wpływ na projekt teorii typów Coqa.

Dominic Mulligan
źródło