IsaMorph

IsaMorph은 대화 형 정리의 증명 이사벨을 갖춘 (Morphix 기준) 리눅스 배포판 라이브 CD입니다.
이것은 당신이 CD로 부팅와 GNU / 리눅스 또는 이자벨를 설치하지 않고 완벽하게 작동 "정리 증명"환경을 얻을 수있는 것을 의미한다. 그냥 PC에 CD를 삽입하고 첫 번째 정리 입증 오분 후에 있습니다.
IsaMorph 내에서 분산 모든 프로그램은 무료 소프트웨어입니다. 이는 운영 시스템이 CD에 포함 된 응용 프로그램은 자유롭게 복사, 수정 및 배포 될 수 있다는 것을 의미한다. 그래서 친구 나 동료에게 사본을 제공 주시기 바랍니다.
인텔 호환 PC 또는 노트북의 CD 드라이브에 CD를 넣습니다. 이제 컴퓨터를 재부팅합니다. 첫 번째 부팅 장치가 CD인지 확인하십시오. 이를 위해, 당신은 당신의 컴퓨터의 BIOS 설정을 변경해야 할 수 있습니다.
당신이 익숙하지 않은 경우, 시스템 관리자 또는 작업을 수행하는 방법을 아는 사람으로부터 도움을받을. 컴퓨터가 부팅 시작되면 드라이브에 CD를 검색합니다. 메뉴가 잠시 후 나타납니다.
그냥 키를 입력하거나 시간을 기다릴 키를 누릅니다. 컴퓨터가 CD로 부팅하고, 희망, 당신이 잘 알고있는 것과 유사한 그래픽 화면을 제공 할 것입니다. 당신은 왼쪽 상단에있는 메뉴를 클릭하고 응용 프로그램을 시작할 수 있습니다.
IsaMorph이 증명 및 문서 생성을 지원하는 완벽한 작업 이자벨 환경을 포함,이 포함되어 있습니다 :
이자벨 (버전 2005)
컴파일 적어도 다음과 같은 논리와 상호 작용하는 정리의 증명 이사벨 : 2005 HOL, HOL-단지, ZF, FOL, 및 순수. 따라서, IsaMorph 부팅 후 즉시 이러한 논리의에서 정리를 증명할 수 있습니다. CD는 이사벨의 튜토리얼과 이론 문서의 오프라인 버전이 포함되어 있습니다.
HOL-TestGen (버전 1.1.1)
명세서 계 유닛 테스트에 대한 테스트 케이스 생성기. 그것은 specfication 및 정리 증명 환경 이자벨 / HOL의 상단에 내장되어 있습니다.
증명 일반 (버전 3.6pre)
이자벨위한 강력한 사용자 인터페이스.
뉴저지의 SML (버전 110.56)
표준 ML 환경 컴파일하고 이사벨을 실행에 사용됩니다.
이맥스 (버전 22.0.50)
증명 일반 이사벨의 기본 사용자 인터페이스와 함께 구축 이맥스 편집기.
의 teTeX (버전 2.0.2)
증거 문서의 생성에 사용되는 완전한 LaTeX의 환경을 제공합니다.
기타 응용 프로그램
또한, CD는 또한 공통의 사용을위한 다양한 응용 분야를 포함한다. 그래서 그것은 사용자 친화적 데스크탑 (그놈) 인터넷 브라우저 (모질라) 등을 포함한다. 그냥 많은 자세한 내용을 보려면 메뉴를보십시오. I는 다운로드 크기를 최소화하는 비 이사벨 특정 소프트웨어의 수를 최소화하기 위해 노력했다.
이 릴리스의 새로운 기능 :