IsaMorph

IsaMorph є розподіл Linux Live CD (на основі Morphix) показуючи інтерактивні докази теорем Ізабель.
Це означає, що ви можете завантажитися з компакт-диска і отримати повністю працездатну "докази теорем" довкілля без установки GNU / Linux або Ізабель. Просто вставте компакт-диск в комп'ютер і мати п'ять хвилин по тому ваш перший теорема доведена.
Всі програми, поширювані в IsaMorph є вільним програмним забезпеченням. Це означає, що операційна система і додатки, що містяться в цьому компакт-диску можна вільно копіювати, модифікувати і поширюється. Тому, будь ласка, не соромтеся, щоб дати копії ваших друзів або колег.
Вставте компакт-диск в дисковод компакт-дисків на сумісному ПК або ноутбук Intel. Тепер перезавантажте комп'ютер. Переконайтеся, що першим завантажувальним пристроєм CD-це. Для цього вам, можливо, доведеться змінити налаштування BIOS вашого комп'ютера.
Якщо ви не знайомі з ним, отримати допомогу від вашого системного адміністратора або хтось, хто знає, як це зробити. Як комп'ютер починає завантаження, він буде шукати для компакт-диска в приводі. З'явиться меню через деякий час.
Просто натисніть клавішу Enter або почекати деякий час. Комп'ютер буде завантажуватися з компакт-диска і, сподіваюся, дасть вам графічний екран, схожий на те, що ви знайомі з. Ви можете натиснути на меню у верхньому лівому кутку і запуску додатків.
IsaMorph містить повністю робочий Ізабель середу, підтримуючу доказ і документ покоління, це включає в себе:
Ізабель (версія 2005 року)
Інтерактивна докази теорем Ізабель 2005 з, щонайменше наступних логік, складеної в: HOL, HOL-комплекс, ZF ВОЛЗ, і чисто. Таким чином, після завантаження IsaMorph можна відразу довести теореми в будь-якому з цих логік. CD включає в себе автономну версію підручників Ізабель і теорії документації.
HOL-TestGen (версія 1.1.1)
Тест генератор для специфікації на основі модульного тестування. Він побудований на вершині Specfication і докази теорем середовища Ізабель / хол.
Доказ Генеральний (версія 3.6pre)
Потужний користувальницький інтерфейс для Ізабель.
SML Нью-Джерсі (версія 110.56)
Стандартний МЛ навколишнього середовища використовується для складання і виконання Ізабель.
GNU Emacs (версія 22.0.50)
Редактор GNU Emacs, яка будує разом з доказом Генерального основний користувальницький інтерфейс Ізабель.
TETEX (версія 2.0.2)
Повна середу Латекс, використовуваний для генерації докази документів.
Інші програми
Крім того, диск також містить різні додатки для загального користування. Вона включає в себе зручний робочий стіл Gnome () Інтернет-браузер (Mozilla), і так далі. Просто погляньте на меню, щоб дізнатися, багато іншого. Я намагався звести до мінімуму кількість неспецифічного програмного забезпечення Ізабель, щоб звести до мінімуму розмір завантаження.
Що нового в цій версії: