IsaMorph

IsaMorph interaktiv teoremi Prover Isabelle featuring (Morphix əsasında) linux distribution Live CD edir.
Bu CD-dən boot və GNU / Linux və ya Isabelle yüklemeden tam əməliyyat "teoremi sübut" Ətraf mühiti əldə edə bilərsiniz deməkdir. Sadəcə PC CD daxil edin və ilk teorem isbat beş dəqiqə sonra var.
IsaMorph ərzində paylanacaq bütün proqramları pulsuz proqram var. Bu əməliyyat sistemi və bu CD olan applications sərbəst sitemizi redaktə və paylanmış bilər deməkdir. Belə ki, dostları və ya həmkarları nüsxə vermək çekinmeyin.
Intel uyğun PC və ya laptop CD sürücü daxil CD daxil edin. İndi kompüter reboot. Ilk açılış cihaz CD olmasını təmin edir. Bunun üçün, sizin kompüter BIOS ayarlarını dəyişdirmək üçün ola bilər.
Siz tanış deyilsə, sizin sistem administratoru və ya bunu necə bilir kimsə kömək almaq. Kompüter önyükleme başlayır kimi, bu sürücü bir CD üçün axtarış edəcək. A menyu bir müddət sonra görünür.
Yalnız əsas daxil edin və ya bir müddət gözləmək basın. kompüter CD açılış və ümid edirəm ki, siz ilə tanış nə bənzər bir qrafik ekran verməyə davam edəcəyik. Siz üst sol menyu basın və ərizə başlaya bilərsiniz.
IsaMorph sübut və sənəd nəsil dəstəkləyən tam iş Isabelle mühiti var, bu daxildir:
Isabelle (version 2005)
tərtib ən azı aşağıdakı məntiqlə interaktiv teoremi Prover Isabelle 2005: HOL, HOL-Complex, ZF, FOL və Pure. Belə ki, IsaMorph önyükleme sonra dərhal bu məntiq hər hansı teoremləri sübut edə bilər. CD Isabelle nin tutorials və nəzəriyyəsi sənədlərin offline versiyasını ehtiva edir.
HOL-TestGen (version 1.1.1)
Dəqiqləşdirilməsi əsasında vahid test üçün test generator. Bu specfication və teorem isbat ətraf mühit Isabelle / HOL üst inşa edilmişdir.
Proof General (version 3.6pre)
Isabelle üçün güclü istifadəçi interfeysi.
New Jersey SML (version 110.56)
Standard ML Ətraf tərtib və Isabelle həyata keçirilməsi üçün istifadə olunur.
GNU Emacs (version 22.0.50)
Proof Baş Isabelle əsas istifadəçi interfeysi ilə birlikdə qurur GNU Emacs redaktoru.
teTeX (version 2.0.2)
Sübut sənədlərin istehsalı üçün istifadə tam lateks mühit.
Digər proqramlar
Bundan əlavə, CD də ümumi istifadə üçün proqram bir sıra ehtiva edir. Bu, bir istifadəçi dostu masa üstü (Gnome) İnternet brauzer (Mozilla) daxildir. Yalnız daha çox tapmaq üçün menyu bir göz atın. Mən download ölçüsü azaltmaq üçün qeyri Isabelle xüsusi proqram sayı minimuma endirmək üçün cəhd.
Bu Release Yenilikler: