Asystent weryfikacji - Proof assistant

Informacje na temat konferencji naukowej można znaleźć w sekcji Interaktywne dowodzenie twierdzeń (konferencja) .
Nie mylić z interaktywnym systemem dowodowym .
Interaktywna sesja sprawdzania w CoqIDE, pokazująca skrypt dowodowy po lewej stronie i stan dowodu po prawej.

W informatyce i logiki matematycznej , A dowód asystent lub interaktywny twierdzenie Prover to narzędzie, aby pomóc w rozwoju formalnych dowodów poprzez współpracę człowieka z maszyną. Wiąże się to z jakimś rodzajem interaktywnego edytora dowodów lub innym interfejsem , za pomocą którego człowiek może kierować wyszukiwaniem dowodów, których szczegóły są przechowywane, a niektóre kroki zapewnia komputer .

Porównanie systemów

Zobacz także: Typ zależny § Porównanie i Automatyczne dowodzenie twierdzenia § Porównanie
Nazwa Ostatnia wersja Deweloper(zy) Język implementacji Cechy
Logika wyższego rzędu Typy zależne Małe jądro Dowód automatyzacji Dowód przez odbicie Generowanie kodu
ACL2 8,3 Matt Kaufmann i J Strother Moore Wspólne seplenienie Nie Nieopisane 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 Helmut Brandl OCaml tak Nie tak tak Nieznany Jeszcze nie zaimplementowane
Coq 8.13.2 INRIA OCaml tak tak tak tak tak tak
F* magazyn Microsoft Research i INRIA F* tak tak Nie tak tak tak
Światło HOL magazyn John Harrison OCaml tak Nie tak tak Nie Nie
HOL4 Kananaskis-13 (lub repo) Michael Norrish, Konrad Slind i inni Standardowy ML tak Nie tak tak Nie tak
Idrys 2 0.4.0. Edwin Brady Idrys tak tak tak Nieznany Częściowy tak
Izabela Isabelle2021 (luty 2021) Larry Paulson ( Cambridge ), Tobias Nipkow ( München ) i Makarius Wenzel Standardowy ML , Scala tak Nie tak tak tak tak
Pochylać się v3.4.2 Badania firmy Microsoft C++ tak tak tak tak tak Nieznany
LEGO (nie jest powiązany z Lego ) 1.3.1 Randy Pollack ( Edynburg ) Standardowy ML tak tak tak Nie Nie Nie
Mizar 8.1.05 Uniwersytet Białostocki Bezpłatny Pascal Częściowy tak Nie Nie Nie Nie
NuPRL 5 Uniwersytet Cornella Wspólne seplenienie tak tak tak tak Nieznany tak
PVS 6,0 SRI Międzynarodowy Wspólne seplenienie tak tak Nie tak Nie Nieznany
dwanaście 1.7.1 Frank Pfenning i Carsten Schürmann Standardowy ML tak tak Nieznany Nie Nie Nieznany
  • ACL2  – język programowania, teoria logiczna pierwszego rzędu i dowodzenie twierdzeń (w trybie interaktywnym i automatycznym) w tradycji Boyer-Moore.
  • Coq  – który 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.
  • Dowódcy twierdzenia HOL  – Rodzina narzędzi wywodząca się ostatecznie z dowodzenia twierdzenia LCF . W tych systemach rdzeń logiczny stanowi biblioteka ich języka programowania. Twierdzenia stanowią nowe elementy języka i mogą być wprowadzane tylko poprzez „strategie”, które gwarantują logiczną poprawność. Kompozycja strategii daje użytkownikom możliwość tworzenia znaczących dowodów przy stosunkowo niewielkiej liczbie interakcji z systemem. Członkowie rodziny to:
  • IMPS, interaktywny system dowodu matematycznego

Twierdzenie Prover Muzeum to inicjatywa w celu zachowania źródła twierdzenia systemów Prover analizy przyszłych, ponieważ są one istotne / artefakty kultury naukowej. Posiada źródła wielu z wyżej wymienionych systemów.

Interfejsy użytkownika

Popularnym interfejsem dla asystentów dowodu jest oparty na Emacs Proof General, opracowany na Uniwersytecie w Edynburgu . Coq zawiera CoqIDE, który jest oparty na OCaml/ Gtk . Isabelle zawiera Isabelle/jEdit, która jest oparta na jEdit i infrastrukturze Isabelle/ Scala do przetwarzania dowodów zorientowanych na dokumenty. Niedawno Makarius Wenzel opracował również rozszerzenie Visual Studio Code dla Isabelle.

Zobacz też

Uwagi

Bibliografia

Zewnętrzne linki

Katalogi