| Isabelle | |
|---|---|
| Tyyppi | Lauseen todistaja |
| Kehittäjä | Paulson |
| Sisään kirjoitettu | poly/ML ; Scala |
| Käyttöjärjestelmä | GNU/Linux [1] , Microsoft Windows [1] ja macOS [1] |
| Ensimmäinen painos | 1. toukokuuta 1989 |
| Laitteistoalusta | cross-platform |
| uusin versio | Isabelle2021-1 (joulukuu 2021 ) |
| Osavaltio | aktiivinen |
| Lisenssi | BSD |
| Verkkosivusto | isabelle.in.tum.de |
Isabelle on interaktiivinen automaattinen todistustyökalu , joka käyttää korkeamman asteen logiikkaa . Se on toteutettu samalla tyylillä kuin yksi ensimmäisistä tällaisista työkaluista - LCF , ja aivan kuten LCF, se on alun perin kirjoitettu kokonaan Standard ML :ssä [2] . Järjestelmä sisältää kompaktin loogisen ytimen, joka voidaan hyväksyä todeksi ilman lisätodisteita (vaikka tämä ei ole välttämätöntä). Yleisenä työkaluna se toteuttaa metalogista (heikkotyyppinen teoria ), jota käytetään toteuttamaan useita Isabelle-objektilogiikan muunnelmia, kuten ensimmäisen asteen logiikkaa (FOL), korkeamman asteen logiikkaa (HOL) tai Zermelo-Fraenkel-joukkoteoriaa . (ZFC). Yleisimmin käytetty objektilogiikan muunnos on Isabelle / HOL, ja melko vakavaa kehitystä joukkoteorian alalla tehtiin Isabelle / ZF: n avulla.
Päämenetelmä Isabellen todistuksen toteuttamiseksi on korkeamman asteen resoluutiomuunnos , joka perustuu korkeamman asteen yhdistämisalgoritmiin . Interaktiivisena järjestelmänä Isabelle sisältää myös tehokkaat automaattiset päättelytyökalut, kuten termien uudelleenkirjoitusmoottorin, analyyttisen taulukon ratkaisijan , ulkoisia toteutettavuusratkaisijoita eri teorioiden ongelmiin, jotka on yhdistetty erikoistuneen Sledgehammer-ulkoisen liitännän kautta, sekä ulkoisen automaattisen lauseen todistamisen. työkalut. , kuten E ja SPASS . Isabellea on käytetty formalisoimaan lukuisia matematiikan ja tietojenkäsittelytieteen lauseita, kuten Gödelin täydellisyyslause , Gödelin todistus valinnan aksiooman riippumattomuudesta , alkulukujen jakautumista koskeva lause . Isabellea on käytetty myös salausprotokollien muodollisen oikeellisuuden ja ohjelmointikielten semantiikan ominaisuuksien todistamiseen.
Monet Isabellen avulla saaduista muodollisista todisteista ovat julkisesti saatavilla, ja ne on tallennettu Muodollisten todisteiden arkistoon , joka sisältää (vuodesta 2019) vähintään 500 artikkelia, mukaan lukien yli 2 miljoonaa koodiriviä [3] .
Levitetään vapaasti BSD- lisenssillä . Kirjoittaja - Lawrence Paulson ( eng. Lawrence Paulson ), nimi on annettu Gerard Huetin tyttären [4] kunniaksi .
Järjestelmän avulla voit kirjoittaa todisteita kahdella tyylillä - proseduurilla ja deklaratiivisella . Todistuksen menettelytapa määrittelee todistustaktiikkojen ja -menettelyjen soveltamisjärjestyksen. Tämä vastaa tyyliä, jolla tavalliset matemaatikot yleensä työskentelevät, mutta tällaisia todistuksia on yleensä melko vaikea ymmärtää, koska niitä luettaessa tulos, joka aiotaan saada tällaisen todistuksen seurauksena, ei ole ilmeinen.
Deklaratiiviset todisteet, jotka on toteutettu erityisellä sisäänrakennetulla todistuskielellä - Isar - määrittelevät tietyt matemaattiset menettelyt, joita on sovellettava. Ihmisten on helpompi lukea ja tarkistaa ne.
Isabellen uusimmissa versioissa menettelyllinen todistetyyli on poistettu käytöstä. Muodollisten todisteiden arkisto suosittelee myös todisteiden esittämistä deklaratiivisella tyylillä [5] .
Esimerkki päinvastaisesta deklaratiivisesta todistuksesta, joka on kirjoitettu Isarilla (todistus vahvistaa kahden neliöjuuren irrationaalisuuden):
lause sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" todistus olkoon ?x = "sqrt (real 2)" oletetaan "?x ∈ ℚ" sitten saadaan mn :: nat missä sqrt_rat: "¦?x¦ = todellinen m / todellinen n" ja alhaisimmat_termit: "koprime m n" by (sääntö Rats_abs_nat_div_natE) eli "todellinen (m^2) = ?x^2 * todellinen (n^2)" by (auto simp add: power2_eq_square) eli yhtälö : "m^2" = 2 * n^2" käyttäen of_nat_eq_iff power2_eq_squarea fastforcen avulla , joten "2 dvd m^2" simp : llä, joten "2 dvd m" : llä simp : llä on "2 dvd n" -todistus - arvosta ‹2 dvd m› saadaan k , jossa "m =" 2 * k" .. yhtälöllä on "2 * n^2 = 2^2 * k^2" yksinkertaisella , joten "2 dvd n^2" on simp eli "2 dvd n" simp qedilla ja ‹ 2 dvd m › have "2 dvd gcd m n" by (sääntö gcd_greatest) with lowest_terms have "2 dvd 1" by simp eli Väärä käyttäen odd_one by blast qed
Isabellea on käytetty useita kertoja muodollisten menetelmien toteuttamiseen ohjelmisto- ja laitteistojärjestelmien määrittelyssä, kehittämisessä ja todentamisessa.
Vuonna 2009 australialaisessa tutkimuskeskuksessa NICTA toteutetun L4.verified- projektin kehittäjät esittivät ensimmäistä kertaa muodollisen todisteen yleiskäyttöisen käyttöjärjestelmäytimen eli seL4-mikroytimen toiminnallisuudesta. (turvallinen sisäänrakennettu versio L4:stä, joka pystyy toimimaan kovassa reaaliajassa) [6] . Todistuksen on rakentanut ja varmentanut Isabelle/HOL; se sisältää yli 200 tuhatta riviä varmistusskriptiä 7500 rivin C-koodin tarkistamiseksi. Todentaminen kattaa koodin, suunnittelun ja toteutuksen[ määritä ] . Osana todistusta osoitettiin, että C-koodi toteuttaa oikein muodollisen ytimen määrityksen. Todistus paljasti 144 virhettä varhaisessa seL4-ytimen C-koodissa ja noin 150 ongelmaa itse ytimen arkkitehtuurissa ja määrittelyssä.
Kevyt Java - ohjelmointikielelle , jossa käytettiin Isabellea, saatiin todiste tyypin turvallisuudesta [7] .
Paulson-järjestelmän kirjoittaja ylläpitää luetteloa Isabellea käyttävistä tutkimusprojekteista [8] .
On olemassa useita automaattisia lauseiden todistamisjärjestelmiä, jotka ovat ominaisuuksiltaan samanlaisia kuin Isabelle , mukaan lukien: