IsaMorph

IsaMorph est un Live CD de distribution Linux (basé sur Morphix) mettant en vedette le démonstrateur interactif Isabelle.
Cela signifie, vous pouvez démarrer à partir du CD et obtenir un "démonstration de théorèmes" environnement pleinement opérationnel sans avoir à installer GNU / Linux ou Isabelle. Il suffit d'insérer le CD dans votre PC et disposez de cinq minutes plus tard, votre premier théorème prouvé.
Tous les programmes sont distribués au sein IsaMorph logiciel libre. Cela signifie que le système d'exploitation et les applications contenues dans ce CD peuvent être librement copiés, modifiés et distribués. Donc, s'il vous plaît sentir libre de donner des copies à vos amis ou collègues.
Insérez le CD dans le lecteur de CD sur un PC ou un ordinateur portable compatible Intel. Maintenant, redémarrez l'ordinateur. Assurez-vous que le premier périphérique de démarrage est CD. Pour cela, vous pouvez avoir à changer les paramètres du BIOS de votre ordinateur.
Si vous n'êtes pas familier avec elle, obtenir de l'aide auprès de votre administrateur système ou quelqu'un qui sait comment le faire. Comme l'ordinateur démarre le démarrage, il va rechercher un CD dans le lecteur. Un menu apparaîtra après un certain temps.
Appuyez simplement sur la touche Entrée ou attendre pendant un certain temps. L'ordinateur va continuer à démarrer à partir du CD et, nous l'espérons, vous donnera un écran graphique similaire à ce que vous êtes familier avec. Vous pouvez cliquer sur le menu en haut à gauche et lancer des applications.
IsaMorph contient un environnement de travail entièrement Isabelle justificative prouvant et la génération de documents, ce qui inclut:
Isabelle (version 2005)
Le démonstrateur interactif Isabelle 2005 avec au moins les logiques suivantes, établies en: HOL, HOL-Complex, ZF, FOL, et Pure. Ainsi, après le démarrage IsaMorph vous pouvez immédiatement prouver des théorèmes dans aucun de ces logiques. Le CD comprend une version hors ligne des tutoriels d'Isabelle et de la documentation de la théorie.
HOL-TestGen (version 1.1.1)
Un générateur de cas de test pour les tests unitaires de spécification basée. Il est construit sur le dessus de l'environnement et de prouver specfication théorème Isabelle / HOL.
Preuve général (version de 3.6pre)
Une interface utilisateur puissante pour Isabelle.
SML du New Jersey (version 110.56)
Le Standard ML Environnement utilisé pour compiler et exécuter Isabelle.
GNU Emacs (version 22.0.50)
L'éditeur GNU Emacs, qui forme avec le général Preuve interface utilisateur principale d'Isabelle.
teTeX (version 2.0.2)
Un environnement de LaTeX complet utilisé pour la génération de documents de preuve.
Autres applications
En outre, le CD contient également une variété d'applications pour une utilisation courante. Il comprend un bureau convivial (Gnome) d'un navigateur Internet (Mozilla), et ainsi de suite. Il suffit de prendre un regard sur le menu pour savoir beaucoup plus. Je essayé de minimiser le nombre de logiciels spécifiques non Isabelle de minimiser la taille de téléchargement.
Quoi de neuf dans cette version: