IsaMorph

IsaMorph adalah distribusi linux Live CD (berdasarkan Morphix) yang menampilkan prover teorema interaktif Isabelle.
Ini berarti, Anda dapat boot dari CD dan mendapatkan sepenuhnya operasional "teorema" lingkungan tanpa menginstal GNU / Linux atau Isabelle. Hanya memasukkan CD di PC Anda dan memiliki lima menit kemudian teorema pertama terbukti.
Semua program didistribusikan dalam IsaMorph adalah perangkat lunak bebas. Ini berarti bahwa sistem operasi dan aplikasi yang terdapat dalam CD ini dapat digandakan, dimodifikasi dan didistribusikan. Jadi jangan ragu untuk memberikan salinan ke teman Anda atau rekan.
Masukkan CD ke dalam drive CD pada Intel PC atau laptop. Sekarang reboot komputer. Pastikan bahwa perangkat boot pertama adalah CD. Untuk ini, Anda mungkin harus mengubah pengaturan BIOS dari komputer Anda.
Jika Anda tidak terbiasa dengan hal itu, mendapatkan bantuan dari administrator sistem atau seseorang yang tahu bagaimana melakukannya. Sebagai komputer mulai booting, maka akan mencari CD di drive. Sebuah menu akan muncul setelah beberapa waktu.
Hanya tekan tombol Enter atau menunggu untuk beberapa waktu. Komputer akan terus boot dari CD dan, mudah-mudahan, memberikan layar grafis mirip dengan apa yang Anda kenal. Anda dapat mengklik pada menu di kiri atas dan mulai aplikasi.
IsaMorph berisi lingkungan Isabelle bekerja sepenuhnya mendukung pembuktian dan dokumen generasi, ini termasuk:
Isabelle (versi 2005)
The prover teorema interaktif Isabelle tahun 2005 dengan setidaknya logika berikut disusun dalam: HOL, HOL-Complex, ZF, FOL, dan Pure. Dengan demikian, setelah boot IsaMorph Anda segera dapat membuktikan teorema dalam logika ini. CD termasuk versi offline tutorial Isabelle dan dokumentasi teori.
HOL-TestGen (versi 1.1.1)
Sebuah generator ujian bagi spesifikasi berdasarkan unit testing. Hal ini dibangun di atas specfication dan teorema membuktikan lingkungan Isabelle / HOL.
Bukti Umum (versi 3.6pre)
Sebuah User Interface yang kuat untuk Isabelle.
SML dari New Jersey (versi 110,56)
Standard ML Lingkungan digunakan untuk mengkompilasi dan mengeksekusi Isabelle.
GNU Emacs (versi 22.0.50)
GNU Emacs Editor yang membangun bersama-sama dengan Bukti Umum antarmuka pengguna utama Isabelle.
teTeX (versi 2.0.2)
Lingkungan LaTeX lengkap digunakan untuk generasi dokumen bukti.
Aplikasi lainnya
Selain itu, CD juga berisi berbagai aplikasi untuk penggunaan umum. Ini mencakup desktop user-friendly (Gnome) browser Internet (Mozilla), dan sebagainya. Hanya mengambil melihat menu untuk mencari tahu lebih banyak. Saya mencoba untuk meminimalkan jumlah perangkat lunak non Isabelle khusus untuk meminimalkan ukuran download.
Apa yang Baru di Release ini: