IsaMorph

IsaMorph é uma distribuição Linux Live CD (com base na Morphix) que caracteriza o teorema interativo Isabelle.
Isto significa, você pode inicializar a partir do CD e obter um ambiente de "teoremas" plenamente operacional sem instalar GNU / Linux ou Isabelle. Basta inserir o CD em seu PC e tem cinco minutos mais tarde o seu primeiro teorema provado.
Todos os programas distribuídos dentro IsaMorph são software livre. Isto significa que o sistema operativo e as aplicações contidas neste CD pode ser livremente copiado, modificado e distribuído. Então, por favor sinta-se livre para dar cópias para seus amigos ou colegas.
Insira o CD na unidade de CD em um PC compatível com Intel ou laptop. Agora reinicie o computador. Certifique-se que o primeiro dispositivo de boot é CD. Para isso, você pode ter que alterar as configurações da BIOS de seu computador.
Se você não estiver familiarizado com ele, começar a ajuda de seu administrador de sistema ou alguém que sabe como fazê-lo. À medida que o computador é iniciado a inicialização, ele vai procurar um CD na unidade. Um menu irá aparecer depois de algum tempo.
Basta pressionar a tecla Enter ou esperar por algum tempo. O computador continuará a arrancar a partir do CD e, esperançosamente, dar-lhe uma tela gráfica semelhante ao que você está familiarizado. Você pode clicar no menu no canto superior esquerdo e iniciar aplicações.
IsaMorph contém um ambiente de trabalho totalmente Isabelle comprovativos de documento e geração, o que inclui:
Isabelle (versão 2005)
O teorema interativo Isabelle 2005, com pelo menos os seguintes lógicas compilados em: HOL, HOL-Complex, ZF, FOL, e Pure. Assim, após a inicialização IsaMorph você pode provar imediatamente teoremas em qualquer destas lógicas. O CD inclui uma versão offline de tutoriais de Isabelle e documentação teoria.
HOL-TestGen (versão 1.1.1)
Um gerador de caso de teste para a especificação base de testes de unidade. Ele é construído em cima do specfication e teorema provando ambiente Isabelle / HOL.
Prova Geral (versão 3.6pre)
Uma poderosa interface de usuário para Isabelle.
SML de New Jersey (versão 110,56)
The Standard ML Ambiente utilizado para a elaboração e execução de Isabelle.
GNU Emacs (versão 22.0.50)
O editor GNU Emacs que constrói em conjunto com o general Prova da interface do usuário principal do Isabelle.
teTeX (versão 2.0.2)
Um ambiente de látex completo usado para a geração de documentos à prova.
Outras Aplicações
Além disso, o CD também contém uma variedade de aplicações para um uso comum. Ele inclui um desktop user-friendly (Gnome) um navegador de Internet (Mozilla), e assim por diante. Basta dar uma olhada no menu de descobrir muitos mais. Eu tentei minimizar o número de software específico não Isabelle para minimizar o tamanho do download.
O que há de novo nesta versão: