Isabelle (asystentka sprawdzająca)

Izabela
Oryginalni autorzy Lawrence'a Paulsona
Deweloperzy Uniwersytet Cambridge i Uniwersytet Techniczny w Monachium i in.
Pierwsze wydanie 1986
Wersja stabilna
Isabelle2021 / luty 2021 ; 2 lata temu ( 2021-02 )
Napisane w Standardowy ML i Scala
System operacyjny Linux , Windows , macOS
Typ Matematyka
Licencja Licencja BSD
Strona internetowa isabelle .in .tum .de

Zautomatyzowany dowód twierdzeń Isabelle to dowód twierdzeń logiki wyższego rzędu (HOL) , napisany w Standard ML i Scala . Jako w stylu LCF , opiera się na małym rdzeniu logicznym (jądrze) w celu zwiększenia wiarygodności dowodów bez wymagania — ale wspierania — wyraźnych obiektów dowodowych.

Isabelle jest dostępna w elastycznym środowisku systemowym umożliwiającym logicznie bezpieczne rozszerzenia, które obejmują zarówno teorie, jak i implementacje do generowania kodu, dokumentacji i specyficznego wsparcia dla różnych metod formalnych . Można go postrzegać jako IDE dla metod formalnych. W ostatnich latach w Isabelle Archive of Formal Proofs ( Izabela AFP ) zgromadzono znaczną liczbę teorii i rozszerzeń systemu.

Isabelle została nazwana przez Lawrence'a Paulsona na cześć córki Gérarda Hueta .

Program do sprawdzania twierdzeń Isabelle jest wolnym oprogramowaniem , wydanym na poprawionej licencji BSD .

Cechy

Isabelle jest ogólna: zapewnia meta-logikę (teorię słabych typów ), która jest używana do kodowania logiki obiektowej, takiej jak logika pierwszego rzędu (FOL), logika wyższego rzędu (HOL) lub teoria mnogości Zermelo-Fraenkla (ZFC). Najpowszechniej używaną logiką obiektową jest Isabelle/HOL, chociaż w Isabelle/ZF dokonano znaczących zmian w teorii mnogości. Główną metodą dowodu Isabelle jest wersja rozdzielczości wyższego rzędu, oparta na unifikacji wyższego rzędu .

Chociaż Isabelle jest interaktywna, oferuje wydajne narzędzia do automatycznego wnioskowania, takie jak silnik przepisywania terminów i narzędzie do sprawdzania obrazów , różne procedury decyzyjne oraz, za pośrednictwem interfejsu automatyzacji dowodu Sledgehammer , zewnętrzne moduły do ​​rozwiązywania teorii spełnialności (SMT) (w tym CVC4 ) i rozwiązania - opartych na zautomatyzowanych dowodach twierdzeń (ATP), w tym E i SPASS ( Metis metoda dowodu rekonstruuje dowody rozdzielczości generowane przez te ATP). Zawiera również dwa modeli ( generatory kontrprzykładów ): Nitpick i Nunchaku .

Isabelle oferuje lokalizacje , które są modułami tworzącymi strukturę dużych dowodów. Ustawienia regionalne ustalają typy, stałe i założenia w określonym zakresie, dzięki czemu nie trzeba ich powtarzać dla każdego lematu .

Isar („ zrozumiałe, półautomatyczne rozumowanie ”) jest formalnym językiem dowodowym Isabelle. Jest inspirowany systemem Mizar .

Przykładowy dowód

Isabelle umożliwia pisanie dowodów w dwóch różnych stylach, proceduralnym i deklaratywnym . Dowody proceduralne określają szereg taktyk ( funkcje/procedury dowodzenia twierdzeń ), które należy zastosować; chociaż odzwierciedlają procedurę, którą ludzki matematyk może zastosować do udowodnienia wyniku, są one zazwyczaj trudne do odczytania, ponieważ nie opisują wyniku tych kroków. Dowody deklaratywne (obsługiwane przez język dowodowy Isabelle, Isar), z drugiej strony, określają rzeczywiste operacje matematyczne, które należy wykonać, i dlatego są łatwiejsze do odczytania i sprawdzenia przez ludzi.

Styl proceduralny został wycofany w ostatnich wersjach Isabelle. [ potrzebne źródło ]

Na przykład deklaratywny dowód przez sprzeczność w Isar, że pierwiastek kwadratowy z dwóch nie jest racjonalny, można zapisać w następujący sposób. 


  
   
    
        twierdzenie  sqrt2_not_rational:  "sqrt 2 ∉ ℚ"  dowód  niech  ?x =  "sqrt 2"  załóżmy  "?x ∈ ℚ"  wtedy  otrzymamy  mn :: nat  gdzie  sqrt_rat:  "¦?x¦ = m / n"  i  najniższe_wyrażenia:  "względnie pierwsze m n "  przez  (rule Rats_abs_nat_div_natE)  stąd  "m^2 = ?x^2 * n^2"  przez  (auto simp add: power2_eq_square)  stąd  eq:  "m^2 = 2 * n^2"  używając               of_nat_eq_iff power2_eq_square  przez  fastforce  stąd  "2 dvd m^2"  przez  simp  stąd  "2 dvd m"  przez  simp  mieć  dowód  "2 dvd n"  -  z  ‹2 dvd m›  uzyskać  k  gdzie  "m = 2 * k"  ..  z  eq  mieć  "2 * n^2 = 2^2 * k^2"  przez  simp  stąd  "2 dvd n^2"  przez  simp   
         tak więc  „2 dvd n”  przez  simp  qed  z  ‹2 dvd m›  have  „2 dvd gcd m n”  przez  (reguła gcd_greatest)  z  najniższymi terminami  mają  „2 dvd 1”  przez  simp  , stąd  False  przy użyciu  nieparzystego_jeden  przez  blast  qed

Aplikacje

Isabelle została wykorzystana do wspomagania formalnych metod specyfikacji, rozwoju i weryfikacji systemów oprogramowania i sprzętu.

Isabelle została wykorzystana do sformalizowania wielu twierdzeń z matematyki i informatyki , takich jak twierdzenie Gödla o kompletności , twierdzenie Gödla o spójności aksjomatu wyboru , twierdzenie o liczbach pierwszych , poprawność protokołów bezpieczeństwa i właściwości semantyki języka programowania . Jak wspomniano, wiele dowodów formalnych jest przechowywanych w Archiwum Dowodów Formalnych, które zawiera (stan na 2019 r.) Co najmniej 500 artykułów z łącznie ponad 2 milionami linii dowodów.

  • W 2009 roku projekt L4.verified w NICTA stworzył pierwszy formalny dowód poprawności działania jądra systemu operacyjnego ogólnego przeznaczenia: mikrojądro seL4 (bezpieczne wbudowane L4 ) . Dowód jest konstruowany i sprawdzany w Isabelle/HOL i obejmuje ponad 200 000 linii skryptu dowodowego do weryfikacji 7500 linii C. Weryfikacja obejmuje kod, projekt i implementację, a główne twierdzenie stwierdza, że ​​kod C poprawnie implementuje formalną specyfikację jądro. Dowód ujawnił 144 błędy we wczesnej wersji kodu C jądra seL4 i około 150 problemów w każdym projekcie i specyfikacji.

Larry Paulson prowadzi listę projektów badawczych wykorzystujących Isabelle.

Alternatywy

Dalsze informacje: Asystent dowodu § Porównanie systemów

Kilka języków i systemów zapewnia podobną funkcjonalność:

Notatki

Dalsza lektura

Linki zewnętrzne

Pobrano z „ https://en.wikipedia.org/w/index.php?title=Isabelle_(proof_assistant)&oldid=1138137548 ”