| Isabelle | |
|---|---|
| Sorts | Satsbevisare |
| Utvecklaren | Paulson |
| Skrivet i | Poly/ML ; Scala |
| Operativ system | GNU/Linux [1] , Microsoft Windows [1] och macOS [1] |
| Första upplagan | 1 maj 1989 |
| Hårdvaruplattform | plattformsoberoende |
| senaste versionen | Isabelle2021-1 (december 2021 ) |
| stat | aktiva |
| Licens | BSD |
| Hemsida | isabelle.in.tum.de |
Isabelle är ett interaktivt automatiskt korrekturverktyg som använder högre ordningslogik . Det är implementerat i samma stil som ett av de första sådana verktygen - LCF och skrevs, precis som LCF, ursprungligen helt i Standard ML [2] . Systemet innehåller en kompakt logisk kärna, som kan accepteras som sann utan ytterligare bevis (även om detta inte är nödvändigt). Som ett allmänt verktyg implementerar den en metalogik (svag typteori ) som används för att implementera flera varianter av Isabelle objektlogik, såsom första ordningens logik (FOL), högre ordningens logik (HOL) eller Zermelo-Fraenkel mängdteori (ZFC). Den mest använda varianten av objektlogik är Isabelle / HOL, liksom ganska allvarliga utvecklingar inom området för mängdteori genomfördes med hjälp av Isabelle / ZF.
Huvudmetoden för att implementera Isabelles bevis är en variant med högre ordningsupplösning baserad på en enhetsalgoritm av högre ordning . Eftersom Isabelle är ett interaktivt system inkluderar Isabelle också kraftfulla automatiska resonemangsverktyg såsom en termomskrivningsmotor , en analytisk tabelllösare , externa genomförbarhetslösare för problem i olika teorier kopplade via ett specialiserat Sledgehammer externt plug-in-gränssnitt, såväl som extern automatisk satsbevisande verktyg. , såsom E och SPASS . Isabelle har använts för att formalisera många satser från matematik och datavetenskap, såsom Gödels fullständighetssats , Gödels bevis på oberoendet av valets axiom , satsen om fördelningen av primtal . Isabelle har också använts för att bevisa den formella riktigheten av kryptografiska protokoll och egenskaperna hos programmeringsspråkens semantik.
Många av de formella bevis som erhållits med Isabelle är allmänt tillgängliga och lagras i Archive of Formal Proofs , som innehåller (från 2019) minst 500 artiklar, inklusive mer än 2 miljoner rader kod [3] .
Distribueras fritt under BSD-licensen . Författare - Lawrence Paulson ( eng. Lawrence Paulson ), namnet ges för att hedra dottern till Gerard Huet [4] .
Systemet låter dig skriva korrektur i två stilar - procedurmässiga och deklarativa . Den processuella stilen av bevis specificerar sekvensen för tillämpningen av taktik och bevisförfaranden. Detta motsvarar den stil som vanliga matematiker vanligtvis arbetar med, men sådana bevis är vanligtvis ganska svåra att förstå, eftersom det resultat som planeras att erhållas som ett resultat av ett sådant bevis inte är uppenbart när man läser dem.
Deklarativa bevis implementerade i ett speciellt inbyggt korrekturspråk - Isar - anger de specifika matematiska procedurer som måste tillämpas. De är lättare att läsa och kontrollera av människor.
I de senaste versionerna av Isabelle har den processuella bevisstilen förkastats. Arkivet för formella bevis rekommenderar också att bevis presenteras i en deklarativ stil [5] .
Ett exempel på ett deklarativt bevis på motsatsen, skrivet i Isar (beviset bekräftar irrationaliteten i kvadratroten ur två):
sats sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" bevis låt ?x = "sqrt (real 2)" anta "?x ∈ ℚ" erhåll sedan mn :: nat där sqrt_rat: "¦?x¦ = real m / real n" och lowest_terms: "coprime m n" av (regel Rats_abs_nat_div_natE) därav "real (m^2) = ?x^2 * real (n^2)" av (auto simp add: power2_eq_square) därav ekv: "m^2 = 2 * n^2" med of_nat_eq_iff power2_eq_square av fastforce därav "2 dvd m^2" av simp därav "2 dvd m" av simp har "2 dvd n" -bevis - från ‹2 dvd m› erhålla k där "m = 2 * k" .. med eq har "2 * n^2 = 2^2 * k^2" av simp därav "2 dvd n^2" av simp alltså "2 dvd n" av simp qed med ‹2 dvd m › har "2 dvd gcd m n" av (regel gcd_greatest) med lägsta_terms har "2 dvd 1" av simp alltså False med odd_one av blast qed
Isabelle har använts många gånger för att implementera formella metoder för specifikation, utveckling och verifiering av mjukvaru- och hårdvarusystem.
2009 gav utvecklarna av projektet L4.verified , som implementerades vid det australiensiska forskningscentret NICTA , för första gången ett formellt bevis på den funktionella korrektheten hos den generella operativsystemkärnan, nämligen mikrokärnan seL4 (en säker inbyggd version av L4 som kan arbeta i hård realtid) [6] . Beviset byggdes och verifierades av Isabelle/HOL; den innehåller över 200 tusen rader verifieringsskript för att kontrollera 7500 rader C-kod. Verifiering omfattar kod, design och implementering[ specificera ] . Som en del av beviset visades det att C-koden implementerar den formella kärnspecifikationen korrekt. Beviset avslöjade 144 fel i den tidiga seL4-kärnan C-koden och cirka 150 problem vardera i arkitekturen och specifikationen av själva kärnan.
För programmeringsspråket Lightweight Java med Isabelle erhölls ett bevis på typsäkerhet [7] .
En lista över forskningsprojekt [8] som använder Isabelle upprätthålls av författaren till Paulson-systemet.
Det finns ett antal system som bevisar automatiska teorem som liknar Isabelle , inklusive: