IsaMorph

IsaMorph è un Live CD di distribuzione di Linux (sulla base di Morphix) con il teorema prover interattivo Isabelle.
Questo significa che è possibile avviare dal CD e ottenere un "teoremi" ambiente pienamente operativo senza installare GNU / Linux o Isabelle. Basta inserire il CD nel PC e hanno cinque minuti dopo il tuo primo teorema dimostrato.
Tutti i programmi distribuiti all'interno IsaMorph sono software libero. Ciò significa che il sistema operativo e le applicazioni contenute in questo CD può essere copiato, modificato e distribuito. Quindi, non esitate a dare copie ai vostri amici o colleghi.
Inserire il CD nel lettore CD su un PC compatibile Intel o laptop. Ora riavviate il computer. Assicurarsi che il primo dispositivo di avvio è CD. Per questo, potrebbe essere necessario modificare le impostazioni del BIOS del computer.
Se non si ha familiarità con essa, ottenere aiuto dal proprio amministratore di sistema o qualcuno che sa come farlo. All'avvio del computer l'avvio, si cercherà un CD nel drive. Apparirà un menu dopo un certo tempo.
Basta premere il tasto Invio o attendere per qualche tempo. Il computer continuerà a fare il boot da CD e, si spera, vi darà una schermata grafica simile a quello che si ha familiarità con. È possibile fare clic sul menu in alto a sinistra e avviare le applicazioni.
IsaMorph contiene un ambiente completamente funzionante Isabelle sostenere lievitazione e documenti generazione, questo include:
Isabelle (versione 2005)
Il teorema prover interattivo Isabelle 2005 almeno i seguenti logiche compilate: HOL, HOL-Complex, ZF, FOL, e Pure. Così, dopo l'avvio IsaMorph si può dimostrare subito teoremi in una di queste logiche. Il CD include una versione offline di tutorial di Isabelle e documentazione teoria.
HOL-TestGen (versione 1.1.1)
Un generatore di banco di prova per il test delle unità specifica basata. E 'costruito in cima alla specfication e teorema dimostrando ambiente Isabelle / HOL.
Prova generale (versione 3.6pre)
Un potente interfaccia utente per Isabelle.
SML del New Jersey (versione 110.56)
La ML Ambiente standard utilizzato per la compilazione e l'esecuzione di Isabelle.
GNU Emacs (versione 22.0.50)
L'editor GNU Emacs che costruisce insieme con prova generale l'interfaccia utente principale di Isabelle.
teTeX (versione 2.0.2)
Un ambiente LaTeX completo utilizzato per la generazione di documenti di prova.
Altre applicazioni
Inoltre, il CD contiene anche una varietà di applicazioni per un uso comune. Esso comprende un desktop user-friendly (Gnome) un browser Internet (Mozilla), e così via. Basta dare un'occhiata al menu per scoprire molti altri. Ho cercato di ridurre al minimo il numero di non software specifici Isabelle per ridurre al minimo la dimensione del download.
Cosa c'è di nuovo in questo rilascio: