IsaMorph

IsaMorph is 'n Linux-verspreiding Live CD (gebaseer op morphix) met die interaktiewe stelling prover Isabelle.
Dit beteken, kan jy boonop uit die CD en kry 'n ten volle operasioneel "stelling bewys" omgewing sonder die installering van GNU / Linux of Isabelle. Voeg net die CD in jou rekenaar en het vyf minute later jou eerste stelling bewys.
Alle programme versprei binne IsaMorph is gratis sagteware. Dit beteken dat die bedryfstelsel en die aansoeke wat in hierdie CD vrylik gekopieer kan word, verander en versprei. So voel asseblief vry om kopieë te gee aan jou vriende of kollegas.
Plaas die CD in die CD-aandrywer op 'n Intel compatible PC of laptop. Nou herbegin die rekenaar. Maak seker dat die eerste boot toestel CD. Vir hierdie, kan jy die BIOS-instellings van jou rekenaar te verander.
As jy nie vertroud is met dit, kry die hulp van jou stelsel administrateur of iemand wat weet hoe om dit te doen. As die rekenaar begin selflaai, sal dit soek na 'n CD in die aandrywer. 'N Spyskaart sal verskyn na 'n tyd.
Net druk die Enter sleutel of wag vir 'n geruime tyd. Die rekenaar sal voortgaan om te begin vanaf die CD en hopelik 'n grafiese skerm soortgelyk aan wat jy vertroud is met jou gee. Jy kan kliek op die spyskaart by die top links en begin aansoeke.
IsaMorph bevat 'n ten volle werk Isabelle omgewing ondersteun bewys en dokument generasie, hierdie sluit in:
Isabelle (weergawe 2005)
Die interaktiewe stelling prover Isabelle 2005 met ten minste die volgende logika saamgestel: HOL, HOL-kompleks, ZF, FOL, en suiwer. So, na selflaai IsaMorph jy dadelik kan bewys stellings in enige van hierdie logika. Die CD sluit 'n regte weergawe van Isabelle se tutoriale en teorie dokumentasie.
HOL-TestGen (weergawe 1.1.1)
'N toetssaak generator vir spesifikasie gebaseer eenheid toets. Dit is gebou op die top van die specfication en stelling bewys omgewing Isabelle / HOL.
Bewys generaal (weergawe 3.6pre)
'N kragtige gebruikerskoppelvlak vir Isabelle.
SML van New Jersey (weergawe 110,56)
Die Standard ML Omgewing gebruik word vir die opstel en uitvoering van Isabelle.
GNU Emacs (weergawe 22.0.50)
Die GNU Emacs redakteur wat saam bou met bewys Algemene die belangrikste gebruikerskoppelvlak van Isabelle.
tetex (weergawe 2.0.2)
'N Volledige LaTeX-omgewing gebruik word vir die opwekking van dokumente bewys.
Ander toepassings
Daarbenewens het die CD bevat ook 'n verskeidenheid van programme vir 'n algemene gebruik. Dit sluit 'n gebruiker-vriendelike lessenaar (Gnome) 'n internet browser (Mozilla), en so aan. Net 'n blik op die spyskaart vir baie meer uit te vind. Ek het probeer om die aantal nie Isabelle spesifieke sagteware te verminder om die grootte aflaai verminder.
Wat is nuut in hierdie release: