Asystent dowodu

Interaktywna sesja sprawdzająca w CoqIDE, pokazująca skrypt sprawdzający po lewej stronie i stan sprawdzający po prawej.

W informatyce i logice matematycznej asystent dowodu lub interaktywny dowód twierdzenia to narzędzie programowe pomagające w opracowywaniu formalnych dowodów w drodze współpracy człowiek-maszyna. Obejmuje to swego rodzaju interaktywny edytor dowodów lub inny interfejs , za pomocą którego człowiek może kierować wyszukiwaniem dowodów, których szczegóły są przechowywane i niektóre etapy są wykonywane przez komputer .

Porównanie systemów

Nazwa	Ostatnia wersja	Deweloper (y)	Język implementacji	Cechy
Nazwa	Ostatnia wersja	Deweloper (y)	Język implementacji	Logika wyższego rzędu	Typy zależne	Małe jądro	Automatyzacja dowodu	Dowód przez refleksję	Generowanie kodu
Lista ACL2	8.3	Matta Kaufmanna i J. Strothera Moore’a	Wspólny Lisp	NIE	Nietypowane	NIE	Tak	Tak	Już wykonywalny
Agda	2.6.2	Ulf Norell, Nils Anders Danielsson i Andreas Abel ( Chalmers i Göteborg )	Haskell	Tak	Tak	Tak	NIE	Częściowy	Już wykonywalny
Albatros	0,4	Helmuta Brandla	OCaml	Tak	NIE	Tak	Tak	Nieznany	Jeszcze nie zaimplementowane
Kok	8.15.2	INRIA	OCaml	Tak	Tak	Tak	Tak	Tak	Tak
F*	magazyn	Badania Microsoftu i INRIA	F*	Tak	Tak	NIE	Tak	Tak	Tak
Światło HOL	magazyn	Johna Harrisona	OCaml	Tak	NIE	Tak	Tak	NIE	NIE
HOL4	Kananaskis-13 (lub repozytorium)	Michaela Norrisha, Konrada Slinda i innych	Standardowy ML	Tak	NIE	Tak	Tak	NIE	Tak
Idrys	2 0.4.0.	Edwina Brady’ego	Idrys	Tak	Tak	Tak	Nieznany	Częściowy	Tak
Izabela	Isabelle2021 (luty 2021)	Larry Paulson ( Cambridge ), Tobias Nipkow ( Monachium ) i Makarius Wenzel	Standardowy ML , Scala	Tak	NIE	Tak	Tak	Tak	Tak
Pochylać się	v3.4.2 (wydanie oficjalne) v3.39.1 (wydanie społeczności) v4.0.0-m3 (wydanie wstępne)	Leonardo de Moura (Badania Microsoftu )	C++	Tak	Tak	Tak	Tak	Tak	Nieznany
LEGO (niezwiązane z Lego )	1.3.1	Randy Pollack ( Edynburg )	Standardowy ML	Tak	Tak	Tak	NIE	NIE	NIE
Mizar	8.1.05	Uniwersytet Białostocki	Darmowy Pascal	Częściowy	Tak	NIE	NIE	NIE	NIE
NuPRL	5	Uniwersytet Cornella	Wspólny Lisp	Tak	Tak	Tak	Tak	Nieznany	Tak
PVS	6,0	Międzynarodowe SRI	Wspólny Lisp	Tak	Tak	NIE	Tak	NIE	Nieznany
Dwanaście	1.7.1	Franka Pfenninga i Carstena Schürmanna	Standardowy ML	Tak	Tak	Nieznany	NIE	NIE	Nieznany

ACL2 - język programowania, teoria logiczna pierwszego rzędu i dowód twierdzeń (zarówno w trybie interaktywnym, jak i automatycznym) w tradycji Boyera-Moore'a.
Coq – umożliwia wyrażenie twierdzeń matematycznych, mechanicznie sprawdza dowody tych twierdzeń, pomaga znaleźć dowody formalne i wyodrębnia certyfikowany program z konstruktywnego dowodu jego formalnej specyfikacji.
Dowody twierdzeń HOL – rodzina narzędzi wywodzących się ostatecznie z dowodu twierdzeń LCF . W tych systemach rdzeń logiczny stanowi biblioteka ich języka programowania. Twierdzenia reprezentują nowe elementy języka i można je wprowadzić jedynie poprzez „strategie”, które gwarantują poprawność logiczną. Kompozycja strategii daje użytkownikom możliwość tworzenia znaczących dowodów przy stosunkowo niewielkiej liczbie interakcji z systemem. Członkowie rodziny obejmują:
- HOL4 – „główny potomek”, wciąż w fazie aktywnego rozwoju. Obsługa zarówno Moskwy ML , jak i Poly/ML . Posiada licencję w stylu BSD .
- HOL Light – kwitnący „minimalistyczny widelec”. Oparty na OCaml .
- ProofPower – stał się własnością firmy, a następnie powrócił do oprogramowania typu open source. Na podstawie standardowego ML .
IMPS, interaktywny system dowodów matematycznych
Isabelle to interaktywne narzędzie do sprawdzania twierdzeń, następca HOL. Główna baza kodu jest objęta licencją BSD, ale dystrybucja Isabelle zawiera wiele narzędzi dodatkowych z różnymi licencjami.
Jape – oparty na Javie.
Pochylać się
KLOCKI LEGO
Matita – Lekki system oparty na rachunku konstrukcji indukcyjnych.
MINLOG – Asystent dowodu oparty na logice minimalnej pierwszego rzędu.
Mizar – Asystent dowodu oparty na logice pierwszego rzędu, w stylu dedukcji naturalnej i teorii mnogości Tarskiego-Grothendiecka .
PhoX – Asystent dowodu oparty na logice wyższego rzędu, który jest rozszerzalny.
System weryfikacji prototypów (PVS) – język i system sprawdzający oparty na logice wyższego rzędu.
TPS i ETPS – Interaktywne dowodzenie twierdzeń również w oparciu o prosty typ rachunku lambda, ale w oparciu o niezależne sformułowanie teorii logicznej i niezależną implementację.

Interfejsy użytkownika

Popularnym interfejsem dla asystentów sprawdzających jest oparty na Emacsie Proof General, opracowany na Uniwersytecie w Edynburgu .

Coq zawiera CoqIDE, który jest oparty na OCaml/ Gtk . Isabelle zawiera Isabelle/jEdit, który jest oparty na jEdit i infrastrukturze Isabelle/ Scala do przetwarzania korekty zorientowanej na dokumenty. Niedawno Makarius Wenzel opracował także rozszerzenie Visual Studio Code dla Isabelle.

Zobacz też

Automatyczne dowodzenie twierdzeń - poddziedzina automatycznego wnioskowania i logiki matematycznej
Dowód wspomagany komputerowo - Dowód matematyczny przynajmniej częściowo wygenerowany komputerowo
Weryfikacja formalna - Udowodnienie lub obalenie poprawności niektórych zamierzonych algorytmów
Metamath – język formalny i powiązany program komputerowy
Manifest QED - Propozycja komputerowej bazy danych całej wiedzy matematycznej
Teorie modulo spełnialności – Problem logiczny badany w informatyce

Notatki

Barendregt, Henk ; Geuvers, Herman (2001). „18. Asystenci sprawdzający korzystający z systemów typów zależnych” (PDF) . W Robinsonie: Alan JA; Woronkow, Andriej (red.). Podręcznik automatycznego rozumowania . Tom. 2. Elsevier. s. 1149–. ISBN 978-0-444-50812-6 . Zarchiwizowane od oryginału (PDF) w dniu 27.07.2007.
Pfenning, Frank . „17. Ramy logiczne” (PDF) . Podręcznik tom 2 2001 . s. 1065–1148.
Pfenning, Frank (1996). „Praktyka ram logicznych”. W Kirchner, H. (red.). Drzewa w algebrze i programowaniu — CAAP '96 . Notatki z wykładów z informatyki. Tom. 1059. Springer. s. 119–134. doi : 10.1007/3-540-61064-2_33 . ISBN 3-540-61064-2 .
Konstabl, Robert L. (1998). „X. Typy w informatyce, filozofii i logice” . W Buss, SR (red.). Podręcznik teorii dowodu . Studia z logiki. Tom. 137. Elsevier. s. 683–786. ISBN 978-0-08-053318-6 .
Geuvers, H. (luty 2009). „Asystenci dowodu: historia, idee i przyszłość” . Sadhana . 34 (1): 3–25. doi : 10.1007/s12046-009-0001-5 . S2CID 14827467 .
Wiedijk, Freek (2005). „Siedemnastu dowódców świata” (PDF) . Uniwersytet Radboud w Nijmegen.

Linki zewnętrzne

Muzeum Dowodów Twierdzeń
„Wprowadzenie” do certyfikowanego programowania z typami zależnymi .
Wprowadzenie do Asystenta Dowodu Coq (z ogólnym wprowadzeniem do interaktywnego dowodzenia twierdzeń)
Interaktywne dowodzenie twierdzeń dla użytkowników Agda
Lista narzędzi do dowodzenia twierdzeń

Katalogi