IsaMorph

IsaMorph ay isang linux distribution Live CD (batay sa Morphix) na nagtatampok ng mga interactive theorem prover Isabelle.
Ang ibig sabihin nito, maaari kang boot mula sa CD at makakuha ng isang ganap na pagpapatakbo "teorama proving" na kapaligiran na walang pag-install ng GNU / Linux o Isabelle. Kailangan lang ipasok ang CD sa iyong PC at may limang minuto mamaya ang iyong unang theorem napatunayan.
Lahat ng programa ay ipinamamahagi sa loob IsaMorph ay libreng software. Nangangahulugan ito na ang mga operating system at ang mga aplikasyon na nakapaloob sa CD ay maaaring maging malayang makopya, mabago at ipinamamahagi. Kaya huwag mag-atubili na magbigay ng mga kopya sa iyong mga kaibigan o kasamahan.
Ipasok ang CD sa CD drive sa isang Intel katugmang PC o laptop. Ngayon reboot ang computer. Tiyakin na ang unang aparato boot ay CD. Para sa mga ito, maaaring mayroon ka na baguhin ang mga setting ng BIOS sa iyong computer.
Kung hindi ka pamilyar sa mga ito, kumuha ng tulong mula sa iyong system administrator o isang tao na nakakaalam kung paano gawin ito. Bilang nagsisimula booting ang computer, ito ay sa paghahanap para sa isang CD sa drive. Ang isang menu ay lilitaw pagkatapos ng ilang panahon.
Just press ang Enter key o maghintay para sa ilang oras. Ang computer ay patuloy na boot mula sa CD at, sana, bigyan ka ng isang graphical screen na katulad ng kung ano ang ikaw ay pamilyar sa. Maaari mong i-click ang menu sa itaas na kaliwang at simulan ang application.
IsaMorph naglalaman ng isang ganap na nagtatrabaho Isabelle environment na sumusuporta sa proving at dokumento na henerasyon, ito ay kabilang ang:
Isabelle (bersyon 2005)
Ang interactive na theorem prover Isabelle 2005 na may hindi bababa sa mga sumusunod na logics naipon sa: HOL, HOL-Complex, ZF, FOL, at dalisay. Kaya, pagkatapos ng booting IsaMorph maaari mong agad na patunayan ang theorems sa anumang ng mga logics. Ang CD ay nagsasama ng isang offline na bersyon ng mga tutorial Isabelle at babasahin theory.
HOL-TestGen (bersyon 1.1.1)
Ang isang pagsubok na kaso generator para sa detalye batay unit testing. Ito ay itinayo sa tuktok ng specfication at theorem na pinatutunayan na kapaligiran Isabelle / HOL.
Katunayan General (version 3.6pre)
Isang malakas na User Interface para Isabelle.
SML of New Jersey (version 110.56)
Ang Standard ML Environment ginagamit para sa pag-ipon at Isinasagawa Isabelle.
GNU Emacs (version 22.0.50)
Ang GNU Emacs editor na gagawa kasama Katunayan General ang pangunahing user interface ng Isabelle.
teTeX (bersyon 2.0.2)
Ang isang kumpletong kapaligiran LaTeX ginagamit para sa henerasyon ng mga patunay na dokumento.
Iba pang mga Aplikasyon
Sa karagdagan, ito ay naglalaman din ng mga CD sa isang iba't ibang mga application para sa isang karaniwang ginagamit. Ito ay nagsasama ng isang user-friendly desktop (Gnome) ng isang Internet browser (Mozilla), at iba pa. Kailangan lang kumuha ng isang pagtingin sa menu upang malaman kung marami pa. Sinubukan kong i-minimize ang bilang ng mga di Isabelle partikular na software upang i-minimize ang laki ng download.
Ano ang Bago sa Paglabas na ito: