IsaMorph

IsaMorph es un Live CD de distribución de Linux (basado en Morphix) con el demostrador de teoremas Isabelle interactiva.
Esto significa, puede arrancar desde el CD y conseguir un entorno en pleno funcionamiento "demostración de teoremas" sin necesidad de instalar GNU / Linux o Isabelle. Sólo tiene que insertar el CD en su PC y tiene cinco minutos más tarde su primer teorema demostrado.
Todos los programas distribuidos dentro IsaMorph son software libre. Esto significa que el sistema operativo y las aplicaciones contenidas en este CD se pueden copiar libremente, modificados y distribuidos. Así que no dude en dar copias a sus amigos o compañeros de trabajo.
Inserte el CD en la unidad de CD en un PC compatible Intel o portátil. Ahora reinicie el equipo. Asegúrese de que el primer dispositivo de arranque es un CD. Para esto, es posible que tenga que cambiar la configuración del BIOS de su ordenador.
Si usted no está familiarizado con ella, busque ayuda de su administrador de sistema o alguien que sabe cómo hacerlo. A medida que el equipo se inicia el arranque, se buscará un CD en la unidad. Aparecerá un menú después de algún tiempo.
Sólo tiene que pulsar la tecla Intro o esperar algún tiempo. El equipo continuará para arrancar desde el CD y, con suerte, te dan una pantalla gráfica similar a lo que usted está familiarizado. Puede hacer clic en el menú en la parte superior izquierda y iniciar aplicaciones.
IsaMorph contiene un entorno de trabajo totalmente Isabelle apoyar la generación proving y el documento, esto incluye:
Isabelle (versión 2005)
El demostrador de teoremas interactiva Isabelle 2005 con al menos los siguientes lógicas compiladas en: HOL, HOL-Complex, ZF, FOL, y puro. Por lo tanto, después de arrancar IsaMorph puedes probar teoremas de inmediato en cualquiera de estas lógicas. El CD incluye una versión offline de tutoriales de Isabelle y documentación teoría.
HOL-TestGen (versión 1.1.1)
Un generador de casos de prueba para las pruebas unitarias especificación basada. Está construido en la parte superior de la specfication y el teorema demostrando entorno Isabelle / HOL.
General de Prueba (versión 3.6pre)
Una interfaz de usuario de gran alcance para Isabelle.
SML de Nueva Jersey (versión 110.56)
El ML Ambiente Estándar utilizado para compilar y ejecutar Isabelle.
GNU Emacs (versión 22.0.50)
El editor GNU Emacs que construye junto con el general Prueba de la interfaz de usuario principal de Isabelle.
teTeX (versión 2.0.2)
Un entorno LaTeX completa que se utiliza para la generación de documentos de prueba.
Otras aplicaciones
Además, el CD también contiene una variedad de aplicaciones para un uso común. Incluye un escritorio fácil de usar (Gnome) un navegador de Internet (Mozilla), y así sucesivamente. Basta con echar un vistazo al menú para descubrir muchos más. Traté de minimizar el número de software específico no Isabelle para minimizar el tamaño de la descarga.
¿Qué hay de nuevo en esta versión: