IsaMorph

IsaMorph egy Linux disztribúció Live CD-(alapján Morphix) jellemző az interaktív bankterminál Isabelle.
Ez azt jelenti, akkor boot a CD, és kap egy teljes mértékben működőképes "tételbizonyítás" környezet telepítése nélkül GNU / Linux vagy Isabelle. Csak helyezze be a CD-t a PC és öt perccel később az első tétel bizonyult.
Minden program keretében kiosztásra IsaMorph vannak szabad szoftver. Ez azt jelenti, hogy az operációs rendszer és az alkalmazások az ebben CD szabadon másolható, módosítható és terjeszthető. Tehát ne habozzon, hogy másolatokat barátaival vagy kollégáival.
Helyezze be a CD-t a CD-meghajtó egy Intel-kompatibilis PC vagy laptop. Most indítsa újra a számítógépet. Győződjön meg arról, hogy az első boot device van CD. Ehhez lehet, hogy változtassa meg a BIOS-beállítások a számítógép.
Ha nem ismeri azt, hogy segítséget kérjen a rendszergazdától, vagy valaki, aki tudja, hogyan kell csinálni. Amikor elindul a számítógép indításakor, akkor keresni egy CD-t a meghajtóba. Egy menü jelenik meg egy idő után.
Csak nyomja meg az Enter billentyűt, vagy várjon egy ideig. A számítógép továbbra is boot a CD, és remélhetőleg, kapsz egy grafikus képernyő hasonlít ahhoz, amit Ön ismeri. Akkor kattints a menü a bal felső sarokban, és indítsa el az alkalmazásokat.
IsaMorph tartalmaz egy teljesen működő Isabelle támogató környezet bizonyító és dokumentum-termelés, ez magában foglalja:
Isabelle (version 2005)
Az interaktív bankterminál Isabelle 2005, legalább a következő logika összeállított: HOL, HOL-Complex, ZF, FOL, és tiszta. Így indítás után IsaMorph akkor azonnal bizonyítani tételek ezek közül bármelyik logika. A CD-n elérhető változata Isabelle oktatóanyagok és elmélet dokumentációt.
HOL-TestGen (version 1.1.1)
A teszt generátor specifikáció alapján egység tesztelése. Ebből épült fel a specfication és tételbizonyítás környezet Isabelle / HOL.
Proof Általános (version 3.6pre)
A hatékony felhasználói felület Isabelle.
SML a New Jersey (version 110,56)
A standard ML Környezetvédelmi összeállítására és végrehajtására Isabelle.
GNU Emacs (version 22.0.50)
A GNU Emacs szerkesztő, amely épít együtt Proof Általános fő felhasználói felülete Isabelle.
teTeX (version 2.0.2)
A teljes LaTeX környezet, a generációs igazoló dokumentumoknak.
Egyéb alkalmazások
Ezen túlmenően, a CD is tartalmaz a különböző alkalmazások a közös használatra. Ez magában foglalja a felhasználóbarát asztali (Gnome) egy internet böngészőt (Mozilla), és így tovább. Csak vess egy pillantást a menü, hogy megtudja, sokkal több. Próbáltam minél kevesebb nem Isabelle különleges szoftver minimalizálja a letöltési méret.
Újdonságok ebben a kiadásban: