IsaMorph

IsaMorphは、対話型定理証明イザベルをフィーチャー（Morphixのに基づく）LinuxディストリビューションのライブCDです。
これは、CDから起動し、GNU / Linuxやイザベルをインストールせずに完全に動作「定理証明」環境を得ることができ、ことを意味します。ちょうどあなたのPCにCDを挿入して、5分後にあなたの最初の定理は証明されています。
IsaMorph内に分布するすべてのプログラムはフリーソフトウェアです。これは、オペレーティングシステムと、このCDに含まれているアプリケーションを自由にコピー、変更および配布することができることを意味します。だからあなたの友人や同僚にコピーを与えること自由に感じなさい。
インテル互換のデスクトップPCやノートPCのCDドライブにCDを挿入します。今すぐコンピュータを再起動します。最初のブートデバイスがCDであることを確認してください。このためには、コンピュータのBIOS設定を変更する必要があります。
あなたはそれに慣れていない場合は、システム管理者またはそれを行う方法を知っている人から助けを得ます。コンピュータが起動を開始するように、ドライブにCDを検索します。メニューには、いくつかの時間後に表示されます。
ただ、キー入力するか、いくつかの時間を待つを押してください。コンピュータがCDから起動し、うまくいけば、あなたが精通しているものと同様のグラフィカルな画面を与えるしていきます。あなたは、左上のメニューをクリックし、アプリケーションを起動することができます。
IsaMorphを証明し、ドキュメントの生成をサポートする完全に動作イザベル環境が含まれ、これは含まれています：
イザベル（バージョン2005）
でコンパイルされ、少なくとも以下の論理でインタラクティブな定理証明イザベル2005：HOL、HOL-コンプレックス、ZF、FOL、およびピュア。したがって、IsaMorphの起動後すぐに、これらの論理のいずれかで定理を証明することができます。 CDはイザベルのチュートリアルや理論のドキュメントのオフラインバージョンが含まれています。
HOL-TestGen（バージョン1.1.1）
仕様ベースのユニットテストのためのテストケース生成装置。これはspecficationと定理証明環境イザベル/ HOLの上に構築されます。
証明全般（バージョン3.6pre）
イザベルのための強力なユーザーインターフェイス。
ニュージャージーのSML（バージョン110.56）
標準ML環境はイザベルをコンパイルして実行するために使用されます。
GNU Emacsの（バージョン22.0.50）
証明一般イザベルの主なユーザー·インターフェースと一緒にビルドGNU Emacsエディタ。
teTeXの（バージョン2.0.2）
証明書の生成に使用される完全なLaTeXの環境。
他のアプリケーション
また、CDには、一般的な使用のためのさまざまなアプリケーションが含まれています。これは、というようにユーザーフレンドリーなデスクトップ（Gnomeの）インターネットブラウザ（Mozillaの）、などが含まれます。ただ、多くの詳細を調べるために、メニューを見てみましょう。 Iは、ダウンロードのサイズを最小限に抑えるために、非イザベル特定のソフトウェアの数を最小限にしようとしました。
このリリースの新機能：