IsaMorph 0.9 review
DownloadIsaMorph is a linux distribution Live CD (based on Morphix) featuring the interactive theorem prover Isabelle. This means, you can b
|
|
IsaMorph is a linux distribution Live CD (based on Morphix) featuring the interactive theorem prover Isabelle.
This means, you can boot from the CD and get a fully operational "theorem proving" environment without installing GNU/Linux or Isabelle. Just insert the CD in your PC and have five minutes later your first theorem proven.
All programs distributed within IsaMorph are free software. This means that the operating system and the applications contained in this CD can be freely copied, modified and distributed. So please feel free to give copies to your friends or colleagues.
Insert the CD into the CD drive on an Intel compatible PC or laptop. Now reboot the computer. Ensure that the first boot device is CD. For this, you may have to change the BIOS settings of your computer.
If you are not familiar with it, get help from your system administrator or someone who knows how to do it. As the computer starts booting, it will search for a CD in the drive. A menu will appear after some time.
Just press the Enter key or wait for some time. The computer will continue to boot from the CD and, hopefully, give you a graphical screen similar to what you are familiar with. You can click on the menu at the top left and start applications.
IsaMorph contains a fully working Isabelle environment supporting proving and document generation, this includes:
Isabelle (version 2005)
The interactive theorem prover Isabelle 2005 with at least the following logics compiled in: HOL, HOL-Complex, ZF, FOL, and Pure. Thus, after booting IsaMorph you can immediately prove theorems in any of these logics. The CD includes a offline version of Isabelle's tutorials and theory documentation.
HOL-TestGen (version 1.1.1)
A test case generator for specification based unit testing. It is built on top of the specfication and theorem proving environment Isabelle/HOL.
Proof General (version 3.6pre)
A powerful User Interface for Isabelle.
SML of New Jersey (version 110.56)
The Standard ML Environment used for compiling and executing Isabelle.
GNU Emacs (version 22.0.50)
The GNU Emacs editor which builds together with Proof General the main user interface of Isabelle.
teTeX (version 2.0.2)
A complete LaTeX environment used for the generation of proof documents.
Other Applications
In addition, the CD also contains a variety of applications for a common use. It includes a user-friendly desktop (Gnome) an Internet browser (Mozilla), and so on. Just take a look at the menu to find out many more. I tried to minimize the number of non Isabelle specific software to minimize the download size.
What's New in This Release:
This is release updates all software on the CD, including all base utilities and all Isabelle related software.
Particularly, this is the first release featuring the latest Isabelle version (2005), X-Symbol (3.6pre), and also HOL-TestGen (1.1.1).
IsaMorph 0.9 search tags