IsaMorph v.0.9


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 Isabelles 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. Enhancements: - 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 is a linux distribution Live CD ...

  • GPL
  • 498.6 Mb
  • 331

Review IsaMorph

  • captcha

Other software of Achim D. Brucker
  • svninfo  v.0.7.3svninfo 0.7.3 is considered as a flexible and advanced tool to extract the revision and file information provided by the Subversion revision control system.To present the version information of a document, one needs to extract it from some kind of ...
    New Distribution software
    • Altova SchemaAgent  v.2018r2sp1Altova SchemaAgent is a graphical tool for analyzing and managing XML Schema, XML instance, XSLT, and WSDL file relationships across a project or an enterprise. Visualize and easily manage file associations via its graphical design interface.
    • DwinsHs  v. is a Pascal script for Inno Setup that allows you to download files from the Internet during the installation process, or visit the WEB server script. The FTP, HTTP and HTTPS protocols are supported.
    • PC Guard Software Protection System  v.6.00.0300PC Guard is a professional software protection and licensing system. Easily protect 32bit/64bit Windows and Microsoft .NET framework (.NET versions) applications from illegal distribution and reverse engineering.
    • AntiDuplicate  v.5.4.0Make hardware keys for anti-piracy protection - using your ordinary computer! Software developers can now prepare a hardware key (dongle) from standard USB flash drive. The result is the media for software distribution and USB token at the same time.
    • ISalient - Web Based Survey Software  v.2.0Easy to use, enterprise-level solution for creating and managing web-based surveys of any size or complexity. iSalient allows you to create flexible surveys by dragging and dropping form elements within a web browser. Easily add, edit, stylize, and ...
    • IScale  v.1.0.1iScale 1.0.1 gives you an efficient way for you to track your health. Studies are showing that simply maintaining a journal helps with weight ...