IsaMorph

IsaMorph là một phân phối Linux Live CD (dựa trên Morphix) có tính năng định lý Prover tương tác Isabelle.
Điều này có nghĩa, bạn có thể khởi động từ đĩa CD và có được một hoạt động đầy đủ "định lý minh" môi trường mà không cần cài GNU / Linux hoặc Isabelle. Chỉ cần đưa đĩa CD vào máy tính của bạn và có năm phút sau đó định lý đầu tiên của bạn đã được chứng minh.
Tất cả các chương trình phân phối trong vòng IsaMorph là phần mềm miễn phí. Điều này có nghĩa rằng các hệ điều hành và các ứng dụng chứa trong CD này có thể được tự do sao chép, sửa đổi và phân phối. Vì vậy, xin vui lòng cảm thấy miễn phí để cung cấp cho các bản sao cho bạn bè hoặc đồng nghiệp của bạn.
Bỏ đĩa CD vào ổ CD trên một máy PC tương thích Intel hoặc máy tính xách tay. Bây giờ khởi động lại máy tính. Đảm bảo rằng các thiết bị khởi động đầu tiên là CD. Đối với điều này, bạn có thể phải thay đổi các thiết lập BIOS của máy tính của bạn.
Nếu bạn không quen thuộc với nó, có được sự giúp đỡ từ người quản trị hệ thống của bạn hay một người biết làm thế nào để làm điều đó. Khi máy tính bắt đầu khởi động, nó sẽ tìm kiếm một đĩa CD vào ổ đĩa. Một menu sẽ xuất hiện sau một thời gian.
Chỉ cần nhấn phím Enter hoặc chờ đợi một thời gian. Các máy tính sẽ tiếp tục khởi động từ đĩa CD, và hy vọng, cung cấp cho bạn một màn hình đồ họa tương tự như những gì bạn đã quen thuộc với. Bạn có thể click vào menu ở phía trên bên trái và bắt đầu ứng dụng.
IsaMorph chứa một môi trường làm việc đầy đủ hỗ trợ Isabelle minh và tài liệu thế hệ, điều này bao gồm:
Isabelle (phiên bản 2005)
Định lý Prover tương tác Isabelle 2005 với ít nhất là logic sau đây được biên soạn trong: HOL, HOL-Complex, ZF, FOL, và Pure. Như vậy, sau khi khởi động IsaMorph bạn ngay lập tức có thể chứng minh định lý trong bất kỳ của những logic. Các đĩa CD bao gồm một phiên bản offline của các hướng dẫn của Isabelle và tài liệu lý thuyết.
HOL-TestGen (phiên bản 1.1.1)
Một máy phát điện trường hợp thử nghiệm cho đặc điểm kỹ thuật dựa trên thử nghiệm đơn vị. Nó được xây dựng trên đầu trang của các specfication và định lý chứng minh môi trường Isabelle / HOL.
Proof chung (phiên bản 3.6pre)
Một giao diện người dùng mạnh mẽ cho Isabelle.
SML của New Jersey (phiên bản 110,56)
Các ML Môi trường chuẩn được sử dụng để biên dịch và thực hiện Isabelle.
GNU Emacs (phiên bản 22.0.50)
Các biên tập viên GNU Emacs trong đó xây dựng cùng với Proof chung giao diện chính của Isabelle.
teTeX (phiên bản 2.0.2)
Một môi trường LaTeX hoàn chỉnh được sử dụng để tạo ra các tài liệu chứng minh.
Các ứng dụng khác
Ngoài ra, các đĩa CD cũng có chứa một loạt các ứng dụng cho việc sử dụng phổ biến. Nó bao gồm một máy tính để bàn sử dụng (Gnome) một trình duyệt Internet (Mozilla), và như vậy. Chỉ cần nhìn vào thực đơn để tìm hiểu nhiều hơn nữa. Tôi đã cố gắng để giảm thiểu số lượng các phần mềm cụ thể không Isabelle để giảm thiểu kích thước download.
Có gì mới trong phiên bản này: