| Isabelle | |
|---|---|
| Type | Sætningsbevis |
| Udvikler | Paulson |
| Skrevet i | Poly/ML ; Scala |
| Operativ system | GNU/Linux [1] , Microsoft Windows [1] og macOS [1] |
| Første udgave | 1. maj 1989 |
| Hardware platform | på tværs af platforme |
| nyeste version | Isabelle2021-1 (december 2021 ) |
| Stat | aktiv |
| Licens | BSD |
| Internet side | isabelle.in.tum.de |
Isabelle er et interaktivt automatisk korrekturværktøj , der bruger logik af højere orden . Det er implementeret i samme stil som et af de første sådanne værktøjer - LCF og blev, ligesom LCF, oprindelig skrevet udelukkende i Standard ML [2] . Systemet indeholder en kompakt logisk kerne, som kan accepteres som sand uden yderligere beviser (selvom dette ikke er nødvendigt). Som et generelt værktøj implementerer det en metalogik (svag type teori ), der bruges til at implementere flere varianter af Isabelle objektlogik, såsom første-ordens logik (FOL), højere-ordens logik (HOL) eller Zermelo-Fraenkel mængdeteori (ZFC). Den mest almindeligt anvendte variant af objektlogik er Isabelle / HOL, ligesom ret seriøse udviklinger inden for mængdeteori blev udført ved hjælp af Isabelle / ZF.
Den vigtigste metode til at implementere Isabelles bevis er en højere-ordens opløsningsvariant baseret på en højere ordens foreningsalgoritme . Da Isabelle er et interaktivt system, inkluderer Isabelle også kraftfulde automatiske ræsonnementværktøjer såsom en termomskrivningsmotor , en analytisk tabelløser , eksterne feasibility-løsere til problemer i forskellige teorier forbundet via en specialiseret Sledgehammer ekstern plug-in-grænseflade, samt ekstern automatisk teorembevis værktøjer. , såsom E og SPASS . Isabelle er blevet brugt til at formalisere adskillige sætninger fra matematik og datalogi, såsom Gödels fuldstændighedssætning , Gödels bevis på uafhængigheden af valgaksiomet , sætningen om fordelingen af primtal . Isabelle er også blevet brugt til at bevise den formelle rigtighed af kryptografiske protokoller og egenskaberne ved programmeringssprogs semantik.
Mange af de formelle beviser opnået ved hjælp af Isabelle er offentligt tilgængelige og gemmes i Archive of Formal Proofs , som indeholder (fra 2019) mindst 500 artikler, inklusive mere end 2 millioner linjer kode [3] .
Distribueres frit under BSD-licensen . Forfatter - Lawrence Paulson ( eng. Lawrence Paulson ), navnet er givet til ære for Gerard Huets datter [4] .
Systemet giver dig mulighed for at skrive korrektur i to stilarter - proceduremæssige og deklarative . Den proceduremæssige bevisstil specificerer rækkefølgen af anvendelse af taktik og bevisprocedurer. Dette svarer til den stil, som almindelige matematikere normalt arbejder i, men sådanne beviser er normalt ret svære at forstå, da det resultat, der planlægges opnået som følge af et sådant bevis, ikke er indlysende, når man læser dem.
Deklarative beviser implementeret i et særligt indbygget korrektursprog - Isar - specificerer de specifikke matematiske procedurer, der skal anvendes. De er nemmere at læse og kontrollere af folk.
I nyere versioner af Isabelle er den proceduremæssige bevisstil blevet forældet. Arkivet for formelle beviser anbefaler også, at beviser præsenteres i en deklarativ stil [5] .
Et eksempel på et deklarativt bevis på det modsatte, skrevet i Isar (beviset bekræfter irrationaliteten af kvadratroden af to):
sætning sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" bevis lad ?x = "sqrt (real 2)" antag "?x ∈ ℚ" så få mn :: nat hvor sqrt_rat: "¦?x¦ = real m / real n" og lowest_terms: "coprime m n" af (regel Rats_abs_nat_div_natE) derfor "real (m^2) = ?x^2 * real (n^2)" af (auto simp add: power2_eq_square) deraf eq: "m^2 = 2 * n^2" ved hjælp af of_nat_eq_iff power2_eq_square af fastforce derfor "2 dvd m^2" af simp derfor "2 dvd m" af simp har "2 dvd n" -bevis - fra ‹2 dvd m› opnå k hvor "m = 2 * k" .. med eq har "2 * n^2 = 2^2 * k^2" af simp derfor "2 dvd n^2" af simp således "2 dvd n" af simp qed med ‹2 dvd m › har "2 dvd gcd m n" af (reglen gcd_greatest) med laveste_termer har "2 dvd 1" af simp således False ved hjælp af odd_one af blast qed
Isabelle er blevet brugt mange gange til at implementere formelle metoder i specifikation, udvikling og verifikation af software- og hardwaresystemer.
I 2009 leverede udviklerne af L4.verified- projektet , som blev implementeret i det australske forskningscenter NICTA , for første gang et formelt bevis på den funktionelle korrekthed af den generelle operativsystemkerne, nemlig seL4-mikrokernen (en sikker indbygget version af L4, der kan arbejde i hård realtid) [6] . Beviset blev bygget og verificeret af Isabelle/HOL; den indeholder over 200 tusind linjer med verifikationsscript til at kontrollere 7500 linjer C-kode. Verifikation dækker over kode, design og implementering[ angiv ] . Som en del af beviset blev det vist, at C-koden implementerer den formelle kernespecifikation korrekt. Beviset afslørede 144 fejl i den tidlige seL4 kerne C-kode og omkring 150 problemer hver i arkitekturen og specifikationen af selve kernen.
For letvægts Java -programmeringssproget ved brug af Isabelle blev der opnået et bevis for typesikkerhed [7] .
En liste over forskningsprojekter [8] , der bruger Isabelle, vedligeholdes af forfatteren af Paulson-systemet.
Der er en række automatiske sætningsbevisende systemer, der ligner Isabelle i egenskaber , herunder: