| Izabella | |
|---|---|
| Típusú | Tétel bizonyító |
| Fejlesztő | Paulson |
| Beírva | Poly/ML ; Scala |
| Operációs rendszer | GNU/Linux [1] , Microsoft Windows [1] és macOS [1] |
| Első kiadás | 1989. május 1 |
| Hardver platform | platformközi |
| legújabb verzió | Isabelle2021-1 (2021. december ) |
| Állapot | aktív |
| Engedély | BSD |
| Weboldal | isabelle.in.tum.de |
Az Isabelle egy interaktív automatikus bizonyító eszköz , amely magasabb rendű logikát használ . Ugyanabban a stílusban van megvalósítva, mint az egyik első ilyen eszköz - LCF , és az LCF-hez hasonlóan eredetileg is teljesen Standard ML -ben íródott [2] . A rendszer tartalmaz egy kompakt logikai magot, amely további bizonyítékok nélkül igaznak fogadható el (bár ez nem szükséges). Általános eszközként egy metalogikus (gyenge típusú elméletet ) valósít meg, amelyet az Isabelle objektumlogika számos változatának megvalósítására használnak, mint például az elsőrendű logikát (FOL), a magasabb rendű logikát (HOL) vagy a Zermelo-Fraenkel halmazelméletet. (ZFC). Az objektumlogika leggyakrabban használt változata az Isabelle / HOL, valamint az Isabelle / ZF segítségével meglehetősen komoly fejlesztéseket hajtottak végre a halmazelmélet területén .
Az Isabelle-féle bizonyítás megvalósításának fő módja egy magasabb rendű felbontású változat, amely magasabb rendű egyesítő algoritmuson alapul . Interaktív rendszerként az Isabelle olyan hatékony automatikus érvelési eszközöket is tartalmaz, mint például a kifejezés újraíró motorja, az elemző táblázat megoldója , külső megvalósíthatósági megoldói különféle elméletek problémáihoz, amelyek egy speciális Sledgehammer külső beépülő interfészen keresztül kapcsolódnak össze, valamint külső automatikus tételbizonyítást. eszközök. , például E és SPASS . Isabelle-t számos matematikai és számítástechnikai tétel formalizálására használták, például Gödel teljességi tételét , a választási axióma függetlenségének Gödel-féle bizonyítását, a prímszámok eloszlására vonatkozó tételt . Az Isabelle-t a kriptográfiai protokollok formai helyességének és a programozási nyelvek szemantikája tulajdonságainak bizonyítására is felhasználták .
Az Isabelle segítségével beszerzett formális bizonyítékok közül sok nyilvánosan elérhető, és az Archive of Formal Proofs -ban tárolódik , amely (2019-től) legalább 500 cikket tartalmaz, köztük több mint 2 millió kódsort [3] .
Szabadon terjesztve a BSD licenc alatt . Szerző - Lawrence Paulson ( eng. Lawrence Paulson ), a nevet Gerard Huet lánya tiszteletére adták [4] .
A rendszer kétféle – procedurális és deklaratív – stílusban teszi lehetővé a bizonyítások írását . A bizonyítási eljárási stílus meghatározza a bizonyítási taktika és eljárás alkalmazási sorrendjét. Ez megfelel annak a stílusnak, amelyben a közönséges matematikusok általában dolgoznak, de az ilyen bizonyításokat általában meglehetősen nehéz megérteni, mivel olvasásuk során nem nyilvánvaló az ilyen bizonyítással elérni kívánt eredmény.
A speciális beépített bizonyító nyelven - Isar - megvalósított deklaratív bizonyítások meghatározzák az alkalmazandó konkrét matematikai eljárásokat. Az emberek könnyebben elolvashatják és ellenőrizhetik őket.
Az Isabelle legújabb verzióiban az eljárási bizonyítási stílus elavult. Az Archive of Formal Proofs is javasolja, hogy a bizonyításokat deklaratív stílusban mutassák be [5] .
Példa az ellenkezőjének deklaratív bizonyítására, Isarban (a bizonyíték megerősíti a kettő négyzetgyökének irracionalitását):
tétel sqrt2_not_rational: "sqrt (valós 2) ∉ ℚ" bizonyítás legyen ?x = "sqrt (real 2)" tételezve fel "?x ∈ ℚ", majd kapjuk mn :: nat ahol sqrt_rat: "¦?x¦ = valós m / valós n" és legalacsonyabb_tagok: "coprime m n" by (Rats_abs_nat_div_natE szabály) innen : "real (m^2) = ?x^2 * real (n^2)" by (auto simp add: power2_eq_square) innen eq: "m^2" = 2 * n^2" a_nat_eq_iff power2_eq_square használatával gyorserővel , tehát "2 dvd m^2" egyszerűvel , így a "2 dvd m" a simp "2 dvd n" bizonyítással rendelkezik - ‹2 dvd m›-ből kapjuk k , ahol "m =" 2 * k" .. eq -vel a "2 * n^2 = 2^2 * k^2" egyszerű , így a "2 dvd n^2" a simp , így a "2 dvd n" a simp qed és a ‹2 dvd m › van "2 dvd gcd m n" by (rule gcd_greatest) with lowest_terms have "2 dvd 1" by simp , tehát hamis az odd_one by blast qed
Az Isabelle-t sokszor használták formális módszerek megvalósítására a szoftver- és hardverrendszerek specifikációjában, fejlesztésében és ellenőrzésében.
Az ausztrál NICTA kutatóközpontban megvalósított L4.verified projekt fejlesztői 2009-ben először nyújtottak hivatalos bizonyítékot az általános célú operációs rendszermag, nevezetesen a seL4 mikrokernel funkcionális helyességére. (az L4 biztonságos beépített változata, amely kemény valós időben képes dolgozni) [6] . A bizonyítékot Isabelle/HOL készítette és ellenőrizte; több mint 200 ezer sor ellenőrző szkriptet tartalmaz 7500 sornyi C kód ellenőrzéséhez. Az ellenőrzés a kódra, a tervezésre és a megvalósításra terjed ki[ adja meg ] . A bizonyítás részeként kiderült, hogy a C kód helyesen valósítja meg a formális kernelspecifikációt. A bizonyítás 144 hibát tárt fel a korai seL4 kernel C kódban, és körülbelül 150 problémát magának a kernelnek az architektúrájában és specifikációjában.
Az Isabelle-t használó Lightweight Java programozási nyelv esetében a típusbiztonság igazolását szereztük [7] .
Az Isabelle-t használó kutatási projektek [8] listáját a Paulson-rendszer szerzője vezeti.
Számos automatikus tételbizonyító rendszer létezik, amelyek képességeikben hasonlóak az Isabelle -hez , többek között: