IsaMorph

IsaMorph is een Linux-distributie Live CD (gebaseerd op Morphix) met de interactieve stellingenbewijzer Isabelle.
Dit betekent dat u kunt starten vanaf de cd en krijgen een volledig operationeel "bewijsvoering" omgeving zonder het installeren van GNU / Linux of Isabelle. Steek gewoon de CD in je PC en vijf minuten later uw eerste stelling bewezen.
Alle programma's verdeeld binnen IsaMorph zijn gratis software. Dit betekent dat het besturingssysteem en toepassingen die in deze CD vrij kan worden gekopieerd, gewijzigd en verdeeld. Dus aarzel niet om kopieën te geven aan uw vrienden of collega's.
Plaats de cd in het cd-station op een Intel compatibele pc of laptop. Nu start de computer opnieuw. Zorg ervoor dat de eerste boot device is CD. Hiervoor moet u de BIOS-instellingen van uw computer te veranderen.
Als je niet bekend bent met het, krijgen hulp van de systeembeheerder of iemand die weet hoe het te doen. Als de computer opstart opstarten, zal het zoeken naar een cd in de drive. Een menu verschijnt na enige tijd.
Druk gewoon op de Enter-toets of wacht voor bepaalde tijd. De computer zal doorgaan op te starten vanaf de cd en, hopelijk, een grafisch scherm vergelijkbaar met wat je bekend bent met geven. U kunt klikken op het menu in de linkerbovenhoek en start toepassingen.
IsaMorph bevat een volledig werkende Isabelle milieu ondersteunen rijzen en het genereren van documenten, dit omvat:
Isabelle (versie 2005)
De interactieve stellingenbewijzer Isabelle 2005 met ten minste de volgende logica's opgesteld: HOL, HOL-Complex, ZF, FOL en Pure. Zo, na het opstarten IsaMorph u meteen kunt bewijzen stellingen in een van deze logica. De CD bevat een offline versie van Isabelle's tutorials en theorie documentatie.
HOL-TestGen (versie 1.1.1)
Een testcase generator voor specificatie gebaseerde unit testing. Het is gebouwd op de top van de specfication en stelling te bewijzen milieu Isabelle / HOL.
Proof Algemeen (versie 3.6pre)
Een krachtige gebruikersinterface voor Isabelle.
SML van New Jersey (versie 110,56)
De Standard ML Environment gebruikt voor het samenstellen en uitvoeren van Isabelle.
GNU Emacs (versie 22.0.50)
The GNU Emacs editor die samen bouwt met Proof-generaal van de belangrijkste gebruikersinterface van Isabelle.
teTeX (versie 2.0.2)
Een volledige LaTeX omgeving gebruikt voor het genereren van documenten bewijzen.
Andere toepassingen
Bovendien, de CD bevat ook een verscheidenheid aan toepassingen voor gemeenschappelijk gebruik. Het omvat een gebruikersvriendelijke desktop (Gnome) een internetbrowser (Mozilla), enzovoorts. Neem eens een kijkje op het menu om veel meer uit te vinden. Ik heb geprobeerd om het aantal niet Isabelle specifieke software te minimaliseren om de download grootte te minimaliseren.
Wat is er nieuw in deze release: